% \setcounter{secnumdepth}{-1}

\chapter*{Abstract}

The work presented in this report addresses the program verification problem using the generic symbolic execution framework  that we have proposed in ~\cite{ArusoaieLR2013SLE}.
We present an automatic and  language-independent program verification approach based on symbolic execution. The specification formalism we consider is  Reachability Logic,
a language-independent logic that constitutes an alternative to Hoare logics. Reachability Logic has a sound and relatively complete deduction system, which offers a lot of freedom (but no guidelines)   for constructing proofs. Hence, we propose symbolic execution as a strategy for proof construction. We show that, under reasonable conditions on the semantics of programming languages, our symbolic-execution based Reachability-Logic formula verification  is sound. We present a prototype implementation of the resulting   language-independent verifier as an extension of a generic symbolic execution engine that we are developing in the \K framework.  The verifier is illustrated on programs written in   languages also formally defined in \K.
 

% \setcounter{secnumdepth}{-1}
\chapter{Research description}

\section{Short overview of the thesis - current status}
\label{rd:ov}
There are many frameworks on symbolic execution nowadays but most of them are specialized and optimized for specific languages: Java PathFinder~\cite{DBLP:conf/kbse/PasareanuR10} for Java, PEX~\cite{pex} for C\#, etc. Most of these frameworks have common approaches, the single fact that makes them different is the language they use to perform symbolic execution. All of them make use of {\it symbolic values}; the symbolic execution  of a program generates an {\it execution tree}, where each branch corresponds to a {\it program path}, also called {\it path condition}. Often, the existent frameworks provide interfaces for additional tools like model-checkers or satisfiability solvers. 

In~\cite{ArusoaieLR2013} we proposed a generic framework for symbolic execution which is parametric in the semantics of a programming language. We use the \K operational semantics of a programming language given as a set of rules and we design an algorithm which produces a symbolic semantics, which can be used to run programs symbolically. As a result, the symbolic execution of a program is a path condition; all path conditions can be obtained calling the Maude model-checker. Most of the existing approaches in symbolic execution are focused mainly on program testing, especially in test case generation. In this report our challenge is to use our symbolic execution framework for reasoning about programs, especially for program verification.


% \setcounter{secnumdepth}{-1}
\chapter{Progress report}

\section{Proposed approach}

The \K definition of a language consists in a set of rewrite rules. The programs together with their state are constituents of a special term which is a called configuration. The rewrite rules have the form: $\pi \Ra \pi' \texttt{ when } \phi$, where $\pi$ and $\pi'$ are configuration terms containing variables, and $\phi$ is a first order logic formula. If $\pi$ matches the concrete configuration then it replaces it with $\pi'$ if $\phi$ holds. The \K rewrite rules are particular cases of Reachability Logic formulas. A RL formula has the form $\varphi\Ra\varphi'$ where $\varphi=\pi\land\phi$ is called {\it pattern}. A rewrite rule can be written as $\pi\land\phi\Ra\pi'\land\textbf{true}$. 

In this report we propose an approach which is meant to use the symbolic semantics of a given programming language and a set of program properties given as reachability rules and prove them using a proof system. The proof system is shown is to be sound and the examples shown in this report illustrate how it works in practice.


\section{Main contributions}
The main contributions are a language-independent framework and a tool, based on symbolic execution, for proving  properties of programs expressed in Reachability Logic (RL). 
Our approach amounts to executing  the  proof system of RL in a certain systematic way,  so that the symbolic execution tree for a given set of proof goals becomes a compact representation of the proof trees (in the RL deductive system) for the goals in question. The soundness of the proposed approach is based on  a so-called \emph{circularity principle} for reachability-logic formulas. Soundness also requires that the semantics of the programming language be total (or, at least,  that  it can  be transformed into an  total semantics in a simple way). We implemented the procedure in a prototype tool that extends our language-independent symbolic execution tool~\cite{ArusoaieLR2013SLE} which is part of the \K framework~\cite{rosu-serbanuta-2010-jlap}. The tool is illustrated on  a  parallel  program  written in a  language  also defined in~\K.

\section{Current papers and publications}

The research done until now also produced some interesting results which ended up as publications in different workshops/conferences:
\begin{itemize}
\item The extended \K semantics of OCL has been submitted for publication as a regular paper entitled "Towards a K Semantics for OCL" in the post-proceedings of the \K'11 workshop, held at Cheile Gr{\u a}di{\c s}tei, Bra{\c s}ov, Rom{\^ a}nia.
\item In order to execute real programs \K framework offers a tool called {\tt krun} which is able to execute programs using directly the \K semantics of a programming language. A limitation of it was that it was not able to deal real input/output operations. We added this feature directly to Maude and we published the paper "Making Maude Definitions more Interactive" in the post-proceedings of WRLA'12(Workshop on Rewriting Logic and Applications), held in Tallinn, Estonia.
\item Improving implementation of the \K framework, changing the syntax of the \K language, adding program execution features, and finishing the \K semantics of made the framework evolve to a stable release. We published the paper "Executing Formal Semantics with the K Tool" in the proceedings of the 18th International Symposium on Formal Methods (FM'12), held in Paris, France. Related to the stable release of \K framework, we also submitted "The K Primer (version 2.5)" for publishing in \K'11 post-proceedings.

\item A more technical paper is "Automating Abstract Syntax Tree construction for Context Free Grammars", which aims to automatize the construction of \K specific abstract syntax trees directly from the context free grammar of a language. It was submitted and accepted for publication in post-proceeding of SYNASC 2012, published by Conference Publishing Service (CPS). The paper will be presented at Timi{\c s}oara, Rom{\^ a}nia, on 28$^{th}$ of September, 2012.

\item The results regarding symbolic execution are part of the technical report "A Generic Framework for Symbolic Execution", which was published at INRIA as Rapport de Recherche no. 8189 in December 2012.

\item The main symbolic execution paper ``A Generic Framework for Symbolic Execution'' has been accepted and published in proceedings of SLE (Software Language Engineering) conference, in October 2013, Indianapolis, USA.

\item Our first attempt in using symbolic execution for verification consisted in developing a methodology for creating Hoare Logic verifiers using the \K semantics of a programming language. We published this methodology in ``Engineering Hoare Logic-based Program Verification in K Framework'' at the 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), held in Timi\c{s}oara, 23-26 September 2013, Romania.

\item A more advanced framework for verification of programs using symbolic execution has been published in the Technical Report ``Language-Independent Program Verification Using Symbolic Execution'' at INRIA, RESEARCH REPORT No. 8369, 2013.

\end{itemize}



% \setcounter{secnumdepth}{-1}
\chapter{Technical report}

%\vspace{-2ex}
\section{Introduction}

%\vspace{-1ex}
%
%\dl{De prezentat pe scurt Reachability Logic si de punctat de ce e greu de implementat direct.\\
%- RL pe scurt\\
%- Executia simbolica\\
%- Utilizarea exec. simb. pt verificare (soundness)\\
%- Exemplu gcd\\
%- Totalitatea\\
%- Circularitatea
%}

Reachability Logic (RL)~\cite{rosu-stefanescu-2012-oopsla} is a language-independent  logic for specifying program properties and for defining the formal operational semantics of programming  languages.
%Its formulas are pairs of \emph{patterns} $\rrule{\varphi}{\varphi'}{}$, where each pattern $\varphi\eqbydef\pattern{\pi}{\phi}$ consists of a basic pattern $\pi$. 
%describing a set of program configurations and the constraints $\phi$ the configurations from $\pi$ must satisfy. 
%A RL rule that gives semantics of a piece of code describes the changes over the configuration obtained by the execution of the code. For instance,  a rule like\\[1ex]
%\centerline{$
%\rrule{\pattern{\kall[black]{cfg}{\kall[black]{k}{X\kra C}\kall[black]{env}{M}}}{\true}}{\pattern{\kall[black]{cfg}{\kall[black]{k}{lookup(X,M)\kra C}\kall[black]{env}{M}}}{true}}
%$}\\[1ex] 
%describes the evaluation of a variable $X$, where $M$ is the memory state of the current configuration and $C$ is the rest of the code (the complete description is given in Section~\ref{sec:prelim}).
%
%A RL rule $\rrule{\pattern{\pi}{\phi}}{\pattern{\pi'}{\phi'}}$ specifies the following  property: any terminating computation that starts from a concrete configuration matching $\pi$ and satisfying $\phi$ eventually reaches a configuration matching $\pi'$ and satisfying $\phi'$.
 For instance,
on the \texttt{gcd} program in Fig.~\ref{fig:gcd}, the RL formula
%\vspace*{-4ex}
\begin{equation}\small
\label{eq:specgcd}
\!\rrule{\pattern{\kall[black]{\mathrm{cfg}}{\kall[black]{k}{\mathtt{gcd}}\kall[black]{env}{\texttt{a}{\mapsto}a~\texttt{b}{\mapsto}b}}}{a\!\geq\!0 \wedge b\!\geq\!0}}{\pattern{\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{M}}}{\mathit{lookup(\texttt{x},\!M)\!=\!\mathit{gcd}(a,\!b)}}}\!\!\!\!
%\vspace*{-1.5ex}
\end{equation}
specifies that after the complete execution of the program from a configuration where the program variables \texttt{a}, \texttt{b}  are bound to  non-negative values $a$, $b$, a configuration where the  program variable \texttt{x} is bound to $\mathit{gcd}(a,b)$  is reached. Here,  $\mathit{gcd}$  is a mathematical description of the greatest-common-divisor (with $\mathit{gcd}(0,0) = 0$ by convention) and $\mathit{lookup}$
is a  standard lookup function in  associative maps. 

%A formal description of Reachability-Logic formulas is given later in the paper.

\begin{center}
\begin{figure}[h]
\centering
\begin{minipage}{.3\linewidth}
\begin{verbatim}
x = a;  y = b;
while (y > 0) {
  r = x % y;
  x = y;
  y = r;
}
\end{verbatim}
\end{minipage}
\caption{\label{fig:gcd} \hspace*{-2mm}\mbox{Program\,\texttt{gcd}}}
\end{figure}
\end{center}

Reachability Logic can also be used for defining the  operational semantics of programming languages, such as that of the   language  in which the \texttt{gcd} program is written.
The symbolic execution approach proposed in~\cite{ArusoaieLR2013SLE} automatically transforms  a   language's semantics such that  programs can be executed with   symbolic values. By running  \texttt{gcd} with  the symbolic  values $a,b$ for \texttt{a},\texttt{b} one gets infinitely many computations, induced by the infinitely many   iterations of the \texttt{while} loop. The first  two ones~are: \\[1ex]
\centerline{$
\begin{aligned}
\pattern{\kall[black]{cfg}{\kall[black]{k}{\mathrm{gcd}}\kall[black]{env}{\texttt{a}{\mapsto} a\ \texttt{b}{\mapsto} b}}}{true}\Rightarrow^*
&\pattern{\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\texttt{a}{\mapsto} a\ \texttt{b}{\mapsto} b\ \texttt{x}{\mapsto} a\ \texttt{y}{\mapsto} b\ 
\texttt{r}\mapsto 0}}}{\neg b>0}\\
\pattern{\kall[black]{cfg}{\kall[black]{k}{\mathrm{gcd}}\kall[black]{env}{\texttt{a}{\mapsto} a\ \texttt{b}{\mapsto}b}}}{true}\Rightarrow^*
&\pattern{\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\texttt{a}{\mapsto} a\ \texttt{b}{\mapsto} b\ \texttt{x}{\mapsto} b\ \texttt{y}{\mapsto} a\,\%\,b\ 
\texttt{r}\mapsto a\,\%\,b}}}{}\\
&\pattern{}{b>0 \land \neg a\,\%\,b>0}
\end{aligned}
$}\\[1ex]
%Hence we could (wrongly) conclude that the following reachability formula holds: 
%\\[1ex]
%\centerline{\small$
%\begin{aligned}
%\pattern{\kall[black]{cfg}{\kall[black]{k}{\mathrm{gcd}}\kall[black]{env}{\texttt{a}{\mapsto} a\ \texttt{b}{\mapsto} b}}}{true}\Rightarrow
%&\pattern{\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\texttt{a}{\mapsto} a\ \texttt{b}{\mapsto} b\ \texttt{x}{\mapsto} a\ \texttt{y}{\mapsto} b\ 
%\texttt{r}\mapsto 0}}}{\neg b>0}\\
%&\lor\\
%&\pattern{\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\texttt{a}{\mapsto} b\ \texttt{b}{\mapsto} a\%b\ 
%\texttt{r}\mapsto a\%b}}}{~}\\
%&{b{>}0 \land b{\not=}0\land \neg a\%b{>}0}\\
%&\lor\ldots
%\end{aligned}
%$}\\[1ex]
%It is easy to see that if $b$ is zero, then the execution of the program gets stuck.
Since the values of  (\texttt{x},\texttt{y}) in the final configurations are $(a, b), (b, a\%b), (a\%b, b\%(a\%b)),\ldots$ and knowing that $\mathit{gcd}(x,y) =\mathit{gcd}(y,x\,\%\,y)$, we could (unsoundly) conclude that the program satisfies the specification~(\ref{eq:specgcd}).
This is because the semantics  of the \IMP  language (presented  in the paper), in which the \texttt{gcd} program is written, is not \emph{total} as it does not have a rule for $\%\:0$. 
%In this paper we study the conditions under which using symbolic execution for
%proving RL formulas is sound. These include the totality condition illustrated above.
% In terms of~\cite{rosu-stefanescu-2012-oopsla}, the semantics is not weakly well-defined. 
%If we add a rule for mod zero, the semantics  (weak) well-defined but in that case is safe to use the symbolic execution to prove reachability rules w.r.t. partial correctness.


Reachability Logic's proof system~\cite{rosu-stefanescu-2012-oopsla} is a set of seven inference rules that, for languages whose semantics satisfy certain  reasonable well-formedness conditions,  is sound and complete for proving reachability-logic formulas. The proof system is concise and elegant, but its use  in practice for proving nontrivial programs  is difficult, because it gives the user a lot of freedom regarding the order and manner of  rule application, and offers no guidelines for constructing proofs. 
%
%\dl{Din descrierea de mai sus nu reiese care este relatia dintre RL si semanticele totale si asta confuzeaza un pic cititorul. Poate ar trebui spus ca asa cum e data semantica lui IMP, nici RL nu este sound atunci cand se aplica peste ea, nici chiar daca o facem totala. In schimb, daca o facem totala, atunci poate fi transformata in una pentru care RL este sound.}
%\vr{Asta e adevarat dar cred ca e prea devreme pentru a intra in astfel de detalii... suntem abia la pagina 2. Am incercat, in textul pe care l-am adaugat, sa raman  vag in ce priveste proprietatile pe care   soundness-ul sist. deductiv RL le impune.}
%\vspace{-1.2ex}

\paragraph*{Contribution} A language-independent framework and tool, based on symbolic execution, for proving  properties of programs expressed in Reachability Logic. 
Our approach amounts to executing  the  proof system of RL in a certain systematic way,  so that
the symbolic execution tree for a given set of proof goals becomes a compact representation of the proof trees (in the RL deductive system) for the goals in question.
%We show that the symbolic execution soundly reachability-logic verification only for languages whose semantics is \emph{total} and satisfies a condition
%called \emph{weak well-definability}, which is related ti  A semantics is well-definable if it can be transformed into an equivalent well-defined one. A key notion we use here is that of \emph{derivative}.  
% Circularity inference rule that allows to use the goals to be proved as axioms. In order to use the proof system in an efficient way, a systematic and smart handling of the circularities is needed. A similar reasoning is true for the Case Analysis inference rule.
The soundness of the proposed approach is based on  a so-called \emph{circularity principle} for reachability-logic formulas. Soundness also requires that the semantics of the programming language be total (or, at least,  that  it can  be transformed into an  total semantics in a simple way). We implemented the procedure in a prototype tool that extends our language-independent symbolic execution tool~\cite{ArusoaieLR2013SLE} which is part of the \K framework~\cite{rosu-serbanuta-2010-jlap}. The tool is illustrated on  a  parallel  program  written in a  language  also defined in~\K.

%\dl{Trebuie mentionat ca metoda merge numai pentru semantici totale.}
%\vr{done}
%\dl{Aici mai putem pune text sa umplem mai bine pagina.}


%\vspace{-1.3ex}

\paragraph*{Organisation}
After this introduction, Section~\ref{sec:prelim} presents preliminary concepts for the rest of the paper: a formal, generic framework for language definitions; the \K language-definition framework as an instance of the proposed generic framework; and an example of a simple imperative language defined in \K. We also recap the
main ingredients of generic framework for symbolic execution from~\cite{ArusoaieLR2013SLE}, and present the proof system of Reachability Logic~\cite{rosu-stefanescu-2012-oopsla}. Section~\ref{sec:serlv} contains the  core contribution of the paper: an approach for verifying RL formulas by symbolic execution. We show that, under reasonable conditions, symbolic execution is a derived  
rule of the RL proof system and  is thus sound by construction; and symbolic execution trees are compact representations of RL proof trees. We also give a circularity principle saying under which conditions it is sound to use RL goals as hypotheses in proofs of programs. This is essential for
proving programs with infinite state-spaces induced e.g., by  performing an unbounded (symbolic) number of loop iterations or of recursive calls. Section~\ref{sec:tool} describes a prototype verification tool based on our language-independent symbolic execution tool~\cite{ArusoaieLR2013SLE} and its 
application to   a parallel program written in a language  defined in~\K. The paper ends with a description of related work. An appendix  contains the proofs of the technical results in the paper. Our tool (with instructions of use) can be tried online on examples at 
\url{https://fmse.info.uaic.ro/tools/kcheck}.
%
%
%Reachability Logic (RL)~\cite{rosu-stefanescu-2012-oopsla} is a logic that is used for both specifying the formal semantics of programming languages and program properties.
%A formula in RL is a rule $\rrule{\varphi}{\varphi'}{}$ consisting of a pair of \emph{patterns} , where a pattern $\varphi\eqbydef\pattern{\pi}{\phi}$ describes a configuration pattern $\pi$ and the constraints $\phi$ the variables from $\pi$ must satisfy. A RL rule that gives semantics of a piece of code describes the changes over the configuration obtained by the execution of the code. For instance,  a rule like\\[1ex]
%\centerline{$
%\rrule{\pattern{\kall[black]{cfg}{\kall[black]{k}{X\kra C}\kall[black]{env}{M}}}{\true}}{\pattern{\kall[black]{cfg}{\kall[black]{k}{lookup(X,M)\kra C}\kall[black]{env}{M}}}{true}}
%$}\\[1ex] 
%describes the evaluation of a variable $X$, where $M$ is the memory state of the current configuration and $C$ is the rest of the code (the complete description is given in Section~\ref{sec:prelim}).
%A rule $\rrule{\pattern{\pi}{\phi}}{\pattern{\pi'}{\phi'}}$ specifies the following program property (the interpretation is w.r.t. the partial correctness): if the execution starting from a concrete configuration matching $\pi$ and satisfying $\phi$ terminates, then the the final concrete configuration matches $\pi'$ and satisfies $\phi'$. For instance,
%if gcd is the program in Figure~\ref{fig:gcd}, a formula like \\[1ex]
%\centerline{$
%\rrule{\pattern{\kall[black]{\mathrm{cfg}}{\kall[black]{k}{gcd}\kall[black]{env}{\texttt{a}{\mapsto}a~\texttt{b}{\mapsto}b}}}{\true}}{\pattern{\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{M}}}{\mathit{lookup(\texttt{x},M)=\mathit{gcd}(a,b)}}}
%$}\\[1ex] 
%\begin{wrapfigure}{r}{0.3\textwidth}
%\centering
%\begin{minipage}{0.3\textwidth}
%\small
%\begin{verbatim}
%x = a;  y = b;
%while (y > 0) {
%  r = x % y;
%  x = y;
%  y = r;
%}
%\end{verbatim}
%\end{minipage}
%%\vspace*{-1ex}
%\caption{\label{fig:gcd} The program gcd}
%%\vspace*{-4ex}
%\end{wrapfigure}
%specifies that after the complete execution of the program gcd starting in a configuration where the program variable \texttt{a} is boud to the value $a$ and \texttt{b} to $b$, we should get a configuration where the value of the program variable \texttt{x} is equal to the gcd of $a$ and $b$.
%
%Symbolic execution~\cite{arusoaie:hal-00766220} transform the semantical rules such that the programs can be executed when the configurations include symbolic values (variables) and the path condition is collected.
%If we execute the program gcd with the symbolic  values $a,b$ for \texttt{a} respectively \texttt{b}, then we get the following computations:\\[1ex]
%\centerline{\small$
%\begin{aligned}
%\pattern{\kall[black]{cfg}{\kall[black]{k}{\mathrm{gcd}}\kall[black]{env}{\texttt{a}{\mapsto} a\ \texttt{b}{\mapsto} b}}}{true}\Rightarrow^*
%&\pattern{\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\texttt{a}{\mapsto} a\ \texttt{b}{\mapsto} b\ \texttt{x}{\mapsto} a\ \texttt{y}{\mapsto} b\ 
%\texttt{r}\mapsto 0}}}{\neg b>0}\\
%\pattern{\kall[black]{cfg}{\kall[black]{k}{\mathrm{gcd}}\kall[black]{env}{\texttt{a}{\mapsto} a\ \texttt{b}{\mapsto}b}}}{true}\Rightarrow^*
%&\pattern{\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\texttt{a}{\mapsto} a\ \texttt{b}{\mapsto} b\ \texttt{x}{\mapsto} b\ \texttt{y}{\mapsto} a\%b\ 
%\texttt{r}\mapsto a\%b}}}{}\\
%&\pattern{}{b>0 \land b\not=0\land \neg a\%b>0}\\
%\ldots&
%\end{aligned}
%$}\\[1ex]
%Hence we could (wrongly) conclude that the following reachability formula holds: 
%\\[1ex]
%\centerline{\small$
%\begin{aligned}
%\pattern{\kall[black]{cfg}{\kall[black]{k}{\mathrm{gcd}}\kall[black]{env}{\texttt{a}{\mapsto} a\ \texttt{b}{\mapsto} b}}}{true}\Rightarrow
%&\pattern{\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\texttt{a}{\mapsto} a\ \texttt{b}{\mapsto} b\ \texttt{x}{\mapsto} a\ \texttt{y}{\mapsto} b\ 
%\texttt{r}\mapsto 0}}}{\neg b>0}\\
%&\lor\\
%&\pattern{\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\texttt{a}{\mapsto} b\ \texttt{b}{\mapsto} a\%b\ 
%\texttt{r}\mapsto a\%b}}}{~}\\
%&{b{>}0 \land b{\not=}0\land \neg a\%b{>}0}\\
%&\lor\ldots
%\end{aligned}
%$}\\[1ex]
%It is easy to see that if $b$ is zero, then the execution of the program gets stuck.
%Much worse, seeing that the values of the variables (\texttt{x},\texttt{y}) in the final configurations are: $(a, b), (b, a\%b), (a\%b, b\%(a\%b)),\ldots$ and knowing that $\mathit{gcd}(X,Y) =\mathit{gcd}(Y,X\%Y)$, we could (wrongly, again) conclude that the above specification given as a reachability formula holds.
%This happens because the semantics does not include a rule for ${\_}\,\%\,0$ ($b\not=0$ in the final path condition is added by the rule that gives semantics to the mod operator). In terms of~\cite{rosu-stefanescu-2012-oopsla}, the semantics is not (weak) well-defined. 
%Even if we add a rule for mod zero, the semantics remains not (weak) well-defined but in that case is safe to use the symbolic execution to prove reachability rules w.r.t. partial correctness.
%
%In this paper we investigate conditions under which it is safe to use the symbolic execution for proving  reachability rules w.r.t. partial correctness.
%We show that the symbolic execution soundly implements case analysis only if the semantics is \emph{total} and we relax the condition of well-definedness to that of well-definability. A semantics is well-definable if it can be transformed into an equivalent well-defined one. A key notion we use here is that of \emph{derivative}.  
%
%Reachability Logic Proof System~\cite{rosu-stefanescu-2012-oopsla} is a set of seven inference rules that is sound and complete to prove the correctness of the reachability rules w.r.t. the partial correctness. The system is system is compact and elegant, but its use in practice for non-trivial programs becomes a difficult task. The most tricky is the Circularity inference rule that allows to use the goals to be proved as axioms. In order to use the proof system in an efficient way, a systematic and smart handling of the circularities is needed. A similar reasoning is true for the Case Analysis inference rule.
%
%In this paper we show that the symbolic execution can help in applying (a part of ) the proof system in a systematic and efficient way. We present an algorithm that allows to prove a set of reachability rules using themselves as circularities. The soundness of the algorithm is based on the extension of the Circularity Principle~\cite{rosu-lucanu-2009-calco} to the case of reachability formulas.
%
%\vspace*{-3ex}
\paragraph*{Acknowledgments}
This work was partially supported by Contract 161/15.06.2010, SMISCSNR 602-12516 (DAK) and by a BQR grant from the University of Lille.

%\vspace*{-1ex}

\section{Preliminaries}
\label{sec:prelim}
%\vspace*{-1ex}

\subsection{The Ingredients of a Language Definition}
\label{sec:langdef}

In this section we identify the  ingredients of  language definitions in a algebraic and term-rewriting setting.
 A  language $\L$ can be  defined as a triple $(\Sigma, \T, \S)$, consisting of a signature $\Sigma$, a model $\T$, and a set $\S$ of (semantical) rules.%\vspace{-3ex}

\subsubsection*{Signature}
$\Sigma$ is a many-sorted algebraic  signature, which includes  at least  a  sort $\Cfg$ for \emph{configurations} and a sort $\Bool$ for \emph{constraint formulas}. We assume in this paper that the constraint formulas are Boolean terms built with a subsignature  $\Sigma^{\mathsf{Bool}} \subseteq \Sigma$ including the boolean constants and operations\footnote{FOL  formulas can be encoded as terms of sort $\sort{Bool}$ with quantifiers as constructors.}
%\dl{Cred ca nota de subsol trebuie sa fie pusa mai tarziu, cand se introduce relatia $\models$.}
%\vr{prefer sa scot referinta la $\models$ din nota de subsol, dar sa las nota aici...}
$\Sigma$ may also include other   subsignatures for other data sorts, depending on the language $\L$ (e.g., integers,  identifiers, lists, maps,\ldots). Let $\Sigma^\mathsf{Data}$ denote the subsignature of $\Sigma$ consisting of all \emph{data} sorts and their operations. 
We assume that the sort $\Cfg$ and the syntax of  $\L$ are not data, i.e., they are  defined in  $\Sigma \setminus \Sigma^\mathsf{Data}$.
Let $T_\Sigma$ denote the  $\Sigma$-algebra of ground terms and $T_{\Sigma,s}$ denote the set of ground terms of  sort\;$s$. 
Given a sort-wise set of variables $V$, let $T_\Sigma(V)$ denote the free $\Sigma$-algebra of terms with variables, $T_{\Sigma,s}(V)$ denote the set of terms of sort $s$ with variables, and $\var(t)$ denote the set of variables occurring in the term\;$t$. \\
%Finally,  $\Var$ denotes a given sort-wise infinite set of variables. 
%\vspace{-5ex}

\subsubsection*{Model}
We assume given a $\Sigma^\mathsf{Data}$-model $\D$, which interprets the data sorts and their operations.
% We suppose that $\D$ is \emph{reachable}, i.e.,
%for all $d \in \D$ there is a ground term $t \in T_{\Sigma^\mathsf{Data}}$ such that $\D_t = d$.
Let $\T$ denote the free $\Sigma$-model generated by $\D$; thus, 
 $\D$ can be seen as the "arithmetic-logic unit" over which the semantics of $\L$ is given.
 $\T$ interprets the non-data sorts as
 ground terms over the signature 
 $(\Sigma \setminus \Sigma^\mathsf{Data})\cup {\D}$. 
%\vspace{-3ex}

\begin{remark}
The exact mathematical construction of the model $\T$ is as follows. Let $\mathit{Alg}_\Sigma$ denote the category of $\Sigma$-algebras and $\mathit{Alg}_{\Sigma^{\sf Data}}$ the category of the $\Sigma^{\sf Data}$-algebras. The reduct functor ${\_}{\upharpoonright}_{\Sigma^{\sf Data}} : \mathit{Alg}_\Sigma\to\mathit{Alg}_{\Sigma^{\sf Data}}$ sends a $\Sigma$-algebra $M$ into $\Sigma^{\sf Data}$-algebra $M{\upharpoonright}_{\Sigma^{\sf Data}}$, where each data sort $d$ and each operator in $\Sigma^{\sf Data}$ are interpreted as in $M$. The functor ${\_}{\upharpoonright}_{\Sigma^{\sf Data}}$ has an left-adjoint functor $F: \mathit{Alg}_{\Sigma^{\sf Data}}\to \mathit{Alg}_\Sigma$.
The model $\T$ is $F(\D)$. We have the identity $\T{\upharpoonright}_{\Sigma^{\sf Data}}=\D$.
\end{remark}%\vspace{-1ex}

We also assume given a satisfaction relation $(\gamma,\rho)\models b$ between pairs consisting of concrete configurations $\gamma\in\T_{\Cfg}$ and valuations $\rho:\Var\to \D$, and constraint formulas $b\in T_{\Sigma,\Bool}(\Var)$. Since here we consider only constraints expressed as Boolean terms, $\models$ is defined by $(\gamma,\rho)\models b$ iff 
$\rho(b)= {\D}_\true$. 
%\footnote{In the more general case, $\T$ is a $\Sigma\setminus \Sigma^{\tt Bool}$-algebra and the interpretation of the terms of sort {\tt Bool} is given by $\models$. $\Sigma^{\tt Bool}$ consits of the sort \texttt{Bool} and its constructors.}
For simplicity, we often write in the sequel $\true,\false$ instead of ${\D}_\true, {\D}_\false$.%\vspace{-3ex}

\subsubsection*{Rules}
A set $\S$ of semantical rules. Each rule has the form $\rrule{\varphi}{\varphi'}{}$ where $\varphi,\varphi'$ are \emph{patterns} over the set of variables $\Var$. Patterns  are formalised below.
%\vspace{-0.5ex}

\begin{definition}[pattern over a given set of variables~\cite{rosu-stefanescu-2012-oopsla}]
\label{def:pattern}
An \emph{elementary pattern} over a set of variables $V$  is an expression of the form $\pattern{\pi}{\phi}$, where  $\pi\in T_{\Sigma,\Cfg}(V)$  is a \emph{basic pattern} and $\phi\in T_{\Sigma,\Bool}(V)$ is the pattern's \emph{condition}.
If $\gamma\in T_\Cfg$ and $\rho\,{:}V\to\T$ we write  $(\gamma,\rho)\models\pattern{\pi}{\phi}$ for
$\gamma =\rho(\pi)$ and $\rho\models \phi$.
\end{definition}
%\begin{remark}
The above definition is a particular case of a definition in~\cite{rosu-stefanescu-2012-oopsla}. There,  a pattern  is a first-order logic formula with configuration terms as sub-formulas. 
%In this paper we  keep the conjunction notation from first-order logic but separate basic patterns from constraints. %We adopt this convention in the rest of the paper.
%\end{remark}
A basic pattern $\pi$   defines  a set of (concrete) configurations, and the condition~$\phi$  gives additional constraints these configurations must satisfy. 
We  identify   basic patterns $\pi$ with elementary patterns $\pattern{\pi}{\true}$. 
Sample patterns are $\pattern{\kall[black]{cfg}{\kall[black]{k}{I_1\terminal{+}I_2\kra C}\kall[black]{env}{\mathit{Env}}}}{}$ and $\pattern{\kall[black]{cfg}{\kall[black]{k}{I_1\terminal{/}I_2\kra C}\kall[black]{env}{\mathit{Env}}}}{I_2\not=_\mathit{Int}0}$. 
\begin{definition}[rule, transition system]
\label{def:sem}
A \emph{rule} is a pair of patterns over a set of variables $\Var$, of the form $\rrule{\varphi}{\varphi'}{}$. Any set  $\S$  of rules defines a labelled transition system $(\T_\Cfg, \ltran{\phantom{\alpha}}{}{\S})$ such that $\gamma\ltran{\alpha}{}{\S}\gamma'$ iff  $\alpha \eqbydef (\rrule{\varphi}{\varphi'}{}) \in \S$ and $\rho:\Var\to\T$ are such that $(\gamma,\rho)\models \varphi$ and
$(\gamma',\rho)\models \varphi'$.
\end{definition}


%\vspace{-1ex}

\subsection{A Simple Imperative Language and its Definition in \mbox{\large{\K}}}
\label{sec:example}


%\begin{figure}[t]
\begin{figure}[t]
%\vspace*{-8ex}
\begin{center}
\begin{tabular}{ll}
\multicolumn{2}{l}{
$\begin{aligned}
\sort{Id} &::= \textrm{domain of identifiers}\\
\sort{Int} &::= \textrm{domain of integer numbers}\\
\sort{~Bool} &::= \textrm{domain of boolean constants }
\end{aligned}$
}\\
$
\begin{aligned}
&{\nonTerminal{\sort{AExp}}} ::={{\nonTerminal{\sort{Int}}}}&&\mid{{{\nonTerminal{\sort{AExp}}}}\terminal{/}{{\nonTerminal{\sort{AExp}}}}}\,[\textrm{strict}]\\
&\hspace{1.3cm}\mid{{\nonTerminal{\sort{Id}}}}{}&&\mid{{{\nonTerminal{\sort{AExp}}}}\terminal{*}{{\nonTerminal{\sort{AExp}}}}}\,[\textrm{strict}]\\
&\hspace{1.3cm}\mid{({\nonTerminal{\sort{AExp}}})}{}\hspace{-3ex}&&\mid{{{\nonTerminal{\sort{AExp}}}}\terminal{+}{{\nonTerminal{\sort{AExp}}}}}\,[\textrm{strict}]\\
&\hspace{1.3cm}\mid{{{\nonTerminal{\sort{AExp}}}}\terminal{/}{{\nonTerminal{\sort{AExp}}}}}\,[\textrm{strict}]\hspace{-3ex}&&\mid{{{\nonTerminal{\sort{AExp}}}}\terminal{\%}{{\nonTerminal{\sort{AExp}}}}}\,[\textrm{strict}]\\
\end{aligned}
$&$
$
\\
$
\begin{aligned}
{\sort{BExp}}::&={{\nonTerminal{\sort{Bool}}}}{} \mid {({\nonTerminal{\sort{BExp}}})}{}\\
&\mid {{{\nonTerminal{\sort{AExp}}}}\terminal{<=}{{\nonTerminal{\sort{AExp}}}}}\,[\textrm{strict}]\\
&\mid {\terminal{not}{{\nonTerminal{\sort{BExp}}}}}\,[\textrm{strict}]\hspace{-2ex}\\
&\mid {{{\nonTerminal{\sort{BExp}}}}\terminal{and}{{\nonTerminal{\sort{BExp}}}}}\,[\textrm{strict}(1)]\\
\end{aligned}
$&$
$
\\
\multicolumn{2}{l}{
$
\begin{aligned}
{\nonTerminal{\sort{Stmt}}}::&={\terminal{skip}}{}
\mid{\terminal{\{}{\nonTerminal{\sort{Stmt}}}\terminal{\}}}
\mid{{{\nonTerminal{\sort{Stmt}}}}\terminal{;}{{\nonTerminal{\sort{Stmt}}}}}\\
&\mid{{{\nonTerminal{\sort{Id}}}}\terminal{:=}{{\nonTerminal{\sort{AExp}}}}}
\mid{\terminal{while}{{\nonTerminal{\sort{BExp}}}}\terminal{do}{{\nonTerminal{\sort{Stmt}}}}}{}\\
&\mid{\terminal{if}{{\nonTerminal{\sort{BExp}}}}\terminal{then}{{\nonTerminal{\sort{Stmt}}}}\terminal{else}{{\nonTerminal{\sort{Stmt}}}}}\,[\textrm{strict}(1)]
\end{aligned}
$}\\
\multicolumn{2}{l}{
$\sort{Code}::=\sort{AExp}\mid\sort{BExp}\mid\sort{Stmt}\mid \sort{Code}\kra\sort{Code}$}
\end{tabular}
\end{center}
%\vspace*{-3ex}
\caption{\label{fig:impsyn}\K Syntax of IMP}
%\vspace*{-5ex}
\end{figure}
%\end{figure}


%%\vspace*{-17ex}

Our running example is \IMP, a simple imperative language intensively used in research papers. The syntax of \IMP is described in Figure~\ref{fig:impsyn} and is mostly self-explained since it uses a BNF notation. The statements of the language are either assignments, {\it if} statements, {\it while} loops, {\it skip} (i.e., the empty statement), or blocks of statements. The attribute  \textit{strict}  in some production rules means the arguments of the annotated expression/statement are evaluated before the expression/statement itself. If  \textit{strict} is followed by a list of natural numbers then it only concerns  the arguments whose  positions are present in the list.



 The operational semantics of \IMP is given as a set of (possibly conditional) rewrite rules.   The terms to which rules apply are called \textit{configurations}. Configurations typically contain the program to be executed, together with any additional information required for
program execution.

\begin{figure}[t]
%%\vspace*{-1ex}
\begin{center}
$
\begin{array}{ll}
\sort{Cfg}&::=\kall[black]{cfg}{\kall[black]{k}{\sort{Code}}\kall[black]{env}{\sort{Map}_{\mathit{Id},\mathit{Int}}}}
\end{array}
$
%\vspace*{-2ex}
\caption{\label{impcfg}\K Configuration of IMP}
%\vspace*{-4ex}
\end{center}
\end{figure}
The structure of a configuration depends on the language being defined; for \IMP, it consists only of the program code to be executed and an environment mapping variables to values.
 Configurations are written in \K as nested structures of \textit{cells}: for  \IMP, a top cell  $\terminal{cfg}$, having 
 a subcell $\terminal{k}$ containing the code and a subcell $\terminal{env}$ containing the environment (cf.\ Figure~\ref{impcfg}). The code inside the  $\terminal{k}$ cell is represented as a list of computation tasks $C_1\kra C_2\kra\ldots$ to be executed in the given order. Computation tasks are typically statements and expressions.
The environment in the $\terminal{env}$ cell  is  a multiset of bindings of identifiers to values, e.g., 
$\terminal{a}{}\mapsto 3, \terminal{b}{} \mapsto 1$.
\begin{figure}[t]
%\vspace*{-6ex}
\begin{center}
$
\begin{aligned}
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1\terminal{+}I_2}}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1+_{\mathit{Int}}I_2}}}{}\\
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1\terminal{*}I_2}}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1*_{\mathit{Int}}I_2}}}{}\\
&\rrule{\pattern{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1\terminal{/}I_2}}}{I_2\not=_\mathit{Int}0}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1\,/_{\!\mathit{Int}}\,I_2}}}\\
&\rrule{\pattern{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1\terminal{\%}I_2}}}{I_2\not=_\mathit{Int}0}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1\,\%_{\mathit{Int}}\,I_2}}}\\
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1\terminal{<=}I_2}}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1\le_{\mathit{Int}}I_2}}}{}\\
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{\true\terminal{and}B}}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{B}}}{}\\
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{\false\terminal{and}B}}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{\false}}}{}\\
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{\terminal{not}B}}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{\neg B}}}{}\\
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{\terminal{skip}\;}}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{}}}{}\\
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{S_1;S_2}}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{S_1\kra S_2}}}{}\\
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{\terminal{\{}S\terminal{\}}}}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{S}}}{}\\
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{\terminal{if}\true\terminal{then}S_1\terminal{else}S_2}}}
{\kprefix[black]{cfg}{\kall[black]{k}{S_1}}}{}\\
&\rrule{\kprefix[black]{cfg}{\kall[black]{k}{\terminal{if}\false\terminal{then}S_1\terminal{else}S_2}}}
{\kprefix[black]{cfg}{\kall[black]{k}{S_2}}}{}\\
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{\terminal{while}B\terminal{do}S}}}{}{}\\
&{}\quad{\kprefix[black]{cfg}{\kprefix[black]{k}{\terminal{if}B\terminal{then}\terminal{\{}S\terminal{;}
  \terminal{while}B\terminal{do}S\terminal{\}}\terminal{else}\ \terminal{skip}}}}\\
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{X}\kall[black]{env}{M}}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{lookup(X,M)}\kall[black]{env}{M}}}{}\\
&\rrule{\kprefix[black]{cfg}{\kprefix[black]{k}{X\terminal{:=}I}\kall[black]{env}{M}}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{}\kall[black]{env}{update(X,M,I)}}}{}
\end{aligned}
$
\end{center}
%\vspace*{-3ex}
\caption{\label{impsem}\K Semantics of IMP}
%\vspace*{-5ex}
\end{figure}

\noindent The semantics of \IMP is shown in  Figure~\ref{impsem}.  Each rewrite rule from the semantics  specifies how the configuration evolves when the first  computation task from the $\terminal{k}$ cell is executed. Dots in a cell mean that the rest of the cell remains unchanged. \
%Most syntactical constructions require one semantical rule. 
%The exceptions are the conjunction operation  and the $\terminal{if}$ statement, 
%which have  Boolean arguments and require two rules each (one rule per Boolean value).
In addition to the rules shown in Figure~\ref{impsem} the semantics of \IMP includes additional rules induced by the \textit{strict} attribute. For the $\terminal{if}$ statement, which is strict in its first argument, this argument is evaluated  by executing the following  rules:\\[1.5ex]
\centerline{
\fontsize{10}{12}
\selectfont
$\hspace{-1ex}\begin{aligned}
&\kprefix[black]{cfg}{\kall[black]{k}{\terminal{if} \mathit{BE} \terminal{then} S_1\terminal{else} S_2\kra C}} &&\hspace{-2.5ex}\pmb{\Rightarrow}
\kprefix[black]{cfg}{\kall[black]{k}{\mathit{BE}\kra\terminal{if} \square \terminal{then} S_1\terminal{else} S_2\kra C}}\\
&\kprefix[black]{cfg}{\kall[black]{k}{B\kra\terminal{if} \square \terminal{then} S_1\terminal{else} S_2\kra C}} &&\hspace{-2.5ex}\pmb{\Rightarrow} 
\kprefix[black]{cfg}{\kall[black]{k}{\terminal{if} B \terminal{then} S_1\terminal{else} S_2\kra C}}
\end{aligned}
$}\\

Here,  $BE$ ranges over \sort{BExp} $\setminus\{\false,\true\}$, $B$ ranges over the Boolean values $\{\false,\true\}$, and 
$\square$ is a special variable, destined to receive the value of $BE$ once it is computed, typically, by the other   rules in the semantics. 

%\vspace*{-0.5ex}

We show  how the definition of \IMP fits the theoretical framework given in Section~\ref{sec:langdef}.  Nonterminals from the syntax ($\sort{Int}, \sort{Bool}, \sort{AExp}, \ldots)$ are sorts in $\Sigma$. Each production from the syntax defines an operation in $\Sigma$; e.g, the production $\sort{AExp}::=\sort{AExp}\terminal{+}\sort{AExp}$ defines the operation $\_\texttt{+}\_:\sort{AExp}\times \sort{AExp}\to \sort{AExp}$. These operations define the constructors of the result sort. For the  sort $\Cfg$, the only constructor is $\kall[black]{cfg}{\kall[black]{k}{\_}\kall[black]{env}{\_}}:\sort{Code}\times\mathit{Map}_{\it Id,Int}\to\Cfg$. The expression $\kall[black]{cfg}{\kall[black]{k}{X:=I\kra C}\kall[black]{env}{X\mapsto 0\  \mathit{Env}}}$ is a term of $T_\Cfg(\Var)$, where $X$ is a variable of sort \sort{Id},
$I$ is a variable of sort \sort{Int},  $C$ is a variable of sort \sort{Code} (the rest of the computation), and $\it Env$ is a variable of sort $\mathit{Map}_{\it Id,Int}$ (the rest of the environment). The data algebra ${\D}$ interprets \sort{Int} as the set of integers, the operations like $+_{\it Int}$  (cf.\ Figure~\ref{impsem}) as the corresponding usual operation on integers, \sort{Bool} as the set of Boolean values $\{\false,\true\}$, the operation like $\land$ as the usual Boolean operations, the sort $\mathit{Map}_{\it Id,Int}$ as the multiset of maps $X\mapsto I$, where $X$ ranges over identifiers \sort{Id} and $I$ over the integers.
The value of an identifier $X$ is  an  environment $M$ is $\mathit{lookup}(X,M)$,  and the environment $M$, updated
by binding an identifier $X$ to a value $I$, is $\mathit{update}(X,M,I)$. Here, $\mathit{lookup}()$ and $\mathit{update}()$ are operations in a signature $\Sigma^\textsf{Map} \subseteq \Sigma^\textsf{Data}$
of maps.
The other sorts, \sort{AExp}, \sort{BExp}, \sort{Stmt}, and \sort{Code}, are interpreted in the  algebra $\T$ as ground terms
% over a modification of the form~(\ref{eq:T}) of the signature $\Sigma$, 
in which  data subterms are replaced by their interpretations in ${\D}$.  For instance, the term $\terminal{if} 1 >_{Int} 0 \terminal{then} \ 
\terminal{skip} \ \terminal{else} \ \terminal{skip}$  is intepreted as $\terminal{if} {\D}_\true \terminal{then} \ 
\terminal{skip} \ \terminal{else} \ \terminal{skip}$.


\subsection{Symbolic Execution}
\label{sec:sym}
We briefly recap our approach to symbolic execution from~\cite{ArusoaieLR2013SLE}:  a new definition $(\symb{\Sigma},\symb{\T},\symb{\S})$ for a language $\symb{\L}$ is automatically generated from a given   definition $(\Sigma, \T, \S)$ of a language $\L$. The new language $\symb{\L}$ has the same syntax, and its semantics  extends  $\L$'s data domains  with symbolic values and  adapts the  semantical rules  of $\L$ to deal with the new domains.
Then, the symbolic execution of  ${\L}$ programs is the concrete  execution of the corresponding $\symb{\L}$ programs, i.e., 
the application of the rewrite rules in the semantics of  $\symb{\L}$. Building the definition  of  $\symb{\L}$ amounts to
extending the signature $\Sigma$ to  a symbolic signature $\symb{\Sigma}$, extending the $\Sigma$-algebra $\T$ to a $\symb{\Sigma}$-algebra $\symb{\T}$, and  turning the concrete rules~$\S$ into symbolic rules $\symb{\S}$.
We  explain here the last step; additional details are in~\cite{ArusoaieLR2013SLE}.
%%\vspace*{-3ex}
%
%%We then obtain  the symbolic transition system $(\symb{\T}_{\symb{\Cfg}},\tran{\symb{\T}}{\symb{\S}})$  by using Definitions~\ref{def:pattern},\ref{def:sem} for $\symb{\L}$, just like the  transition system $(\T_\Cfg, \tran{\T}{\S})$ was defined for $\L$.
%%Section~\ref{sec:rel} then deals with the relations between the two transition systems.
%
%\subsubsection{Extending the Signature \mbox{{$\Sigma$}} to  a Symbolic Signature \mbox{{$\symb{\Sigma}$}}}
%\label{sec:sigsym}
%
%
%The  signature $\symb{\Sigma}$ extends $\Sigma$  with   a sort $\symb{\Cfg}$ and a constructor $\pattern{\_}{\_}: \Cfg \times \sort{Bool} \to \symb{\Cfg}$, which builds symbolic configurations as patterns over  symbolic values. Specifically, symbolic configurations are \textit{basic}  patterns over symbolic in $\symb{\L}$ according to Definition~\ref{def:pattern} since the symbol $\_\pmb{\wedge}\_$ is part of $\symb{\Sigma}$. Like before, we identify basic patterns 
%$\pattern{\symb{\pi}}{\symb{\phi}}$ in $\symb{\L}$ with elementary patterns $(\pattern{\symb{\pi}}{\symb{\phi}}) \pmb{\wedge} \true$. We thus consider the set  of constraint formulas to be the singleton Boolean term $\{\true\}$. 
%
%
%%\dl{The set of constraint formulas is empty. In practice, a singleton contraint formula $\top$ is used with the following semantics: $(\pattern{\pi}{\phi},\rho)\models \top$ iff $\rho(\phi)$ is not unsatisfiable. Then symbolic patterns of the form   $\pattern{(\pattern{\pi}{\phi})}{\top}$ are used instead of symbolic basic patterns  $\pattern{\pi}{\phi}$.}
%%\vr{alternativa ar fi sa consideram o singura constraint formula, $\true$, cu relatia de satisfactie triviala.}
%
%%\vspace*{-3ex}
%
%\subsubsection{Extending the Model $\T$ to\, a Symbolic Model $\symb{\T}$}
%\label{sec:modelsym}
%We assume an infinite, sort-wise set of \emph{symbolic values} $\symb{V}$ of the data sorts, disjoint from   $\Sigma$ and from the set $\Var$ of variables occuring in the semantical rules $\S$ of the language $\L$. The model
% $\symb{\T}$ is the free $\symb{\Sigma}$-algebra generated by $\D \cup
% \symb{V}$.  In particular, symbolic configurations are (basic) patterns
% $\pattern{\symb{\pi}}{\symb{\phi}}$ over the symbolic values
% $\symb{V}$. We use the superscript $\symb{}$ to indicate the presence
% of  variables in $\symb{V}$ in a term. 
%%Since there is an inclusion signature morphism $\Sigma\hookrightarrow\symb{\Sigma}$, $\symb{\T}$ can also be seen as a $\Sigma$-model $\symb{\T}{\!\upharpoonright}_\Sigma$, where only the interpretations of the symbols  from $\Sigma$ are considered. 
%%\vr{Am fixat algebra $\symb{\T}$; e ceea ce ne trebuie atunci cand verificam formule de RL.}
%
%
%
%%\dl{Since the set of constraint formulas is empty, the only ML formulas are the basic patterns and we have $(\pattern{\symb{\pi}}{\symb{\phi}},\sigma)\models \pattern{\pi}{\phi}$ iff $\sigma(\pattern{\pi}{\phi})=\pattern{\symb{\pi}}{\symb{\phi}}$, where $\sigma:\Var\to\symb{\T}$ is a substitution. Moreover, a concrete symbolic configuration $\pattern{\symb{\pi}}{\symb{\phi}}$ can be seen as an ML formula, hence does make sense to write $(\gamma,\rho)\models\pattern{\symb{\pi}}{\symb{\phi}}$, where $\gamma\in\T_{\Cfg}$ and $\rho:\symb{V}\to \D$.}
%
%%\vspace*{-1ex}
%
%\begin{remark}
%The construction of $\symb{\T}$ is similar to that of $\T$. Let $\mathit{Set}$ denote the category of sets and $U:\mathit{Alg}_{\symb{\Sigma}}\to \mathit{Set}$ the forgetful functor, which sends a $\symb{\Sigma}$-algebra into its carrier set. $U$ has the left-adjoint functor $F:\mathit{Set}\to \mathit{Alg}_{\symb{\Sigma}}$ that sends a set $X$ to the free term algebra $T_\Sigma(X)$. In general, a richer algebra may be needed, e.g., where the ground data terms are identified with their interpretation in $\D$. However, for the purpose of this paper, the above construction is enough.
%%, and all results are preserved if we consider a more powerful symbolic model.
%\end{remark}
%
%%\vspace*{-4ex}
%
%
%\subsubsection{Turning the Concrete Rules $\S$  into Symbolic Rules $\symb{\S}$ }
%\label{sec:semsym}
%%We show how to automatically build the symbolic-semantics rules  $\symb{\S}$ from the concrete semantics-rules $\S$,  by applying the three steps described below.

We  make the following \emph{assumption}: the basic patterns in left-hand sides of rules do not contain operations on data, and the rules are left-linear. These assumptions can be made to hold by rule transformations as shown in~\cite{ArusoaieLR2013SLE}.
Turning concrete rules into symbolic ones consists in transforming  each rule $\rrule{\varphi}{\varphi'}{}\in \S$, with $\varphi \eqbydef \pattern{\pi}{\phi}$
and   $\varphi' \eqbydef \pattern{\pi'}{\phi'}$, into the following one:

%\vspace*{-4ex}

\begin{eqnarray}
&& \rrule{\pattern{ \pi}{\psi}}{\pattern{\pi'}{(\psi \land \phi \wedge \phi')}}{} \label{eq:transform}
\end{eqnarray}

%\vspace*{-1ex}


\noindent 
where $\psi \in \Var$ is a fresh variable of sort $\sort{Bool}$ playing the role of a path condition.
This means that symbolic rule  are applied like concrete rules, except for the fact that the current path condition $\psi$ is enriched with the rule's conditions $\phi,\phi'$.

\begin{example}

The first rule for $\terminal{if}$ from the  \IMP semantics is transformed into the following rule in $\symb{\S}$, by applying the various transformations from~\cite{ArusoaieLR2013SLE}:

%\vspace*{-4ex}

\begin{align*}
\fontsize{9}{10}
\selectfont
&\kprefix[black]{cfg}{\kprefix[black]{k}{\terminal{if}B\terminal{then}S_1\terminal{else}S_2}} \pmb{\wedge} \psi \pmb{\Rightarrow}
\kprefix[black]{cfg}{\kprefix[black]{k}{S_1}} \pmb{\wedge} {\psi{\land}(B = \true)}
\end{align*}
\end{example}
%%\vspace*{-4ex}
%
%
%
%\subsubsection{Defining the Symbolic Transition System }
%\label{subsec:step3}
The triple ($\symb{\Sigma}$, $\symb{\T}$,   $\symb{\D}$)  defines a language $\symb{\L}$. Then, the
 transition system  $(\symb{\T}_{\symb{\Cfg}},\tran{}{\symb{\S}})$ is defined using Definitions~\ref{def:pattern},~\ref{def:sem} applied to $\symb{\L}$.
% Specifically, Definition~\ref{def:sem} applied to  $\symb{\L}$ defines the symbolic transition system; in the  statement $(\pattern{\symb{\pi}}{\symb{\phi}},\rho) \models \varphi $ occurring in this definition,
% $\rho$ has co-domain $\symb{\T}$, and the satisfaction  $\models$ is  given by Definition~\ref{def:pattern} for $\symb{\L}$.
%For this, we    note that the
%left-hand sides of the rules of $\symb{\L}$, of the form $\langle \pi, \psi \rangle$, are terms in $T_{\symb{\Sigma}, \symb{\Cfg}}(\Var)$.
%Since $\pattern{\pi}{\phi}$ and  $\pattern{\pi'}{\phi'}$ are patterns of $\L$, it follows,  according to   Definition~\ref{def:pattern} applied to  $\symb{\L}$, that 
%  $ \pattern{\pattern{ \pi}{\psi}}{}$ and  $ \pattern{\pattern{\pi'}{(\psi \land \phi \wedge \phi')}}{}$   are (basic!) patterns of   $\symb{\L}$, and  then Definition~\ref{def:sem}  for $\symb{\L}$ gives us
%  the transition system $(\symb{\T}_{\symb{\Cfg}},\tran{}{\symb{\S}})$.
%\vr{de explicat de ce $\pattern{\pattern{ \pi}{\psi}}{}$ este  basic pattern in $\symb{\L}$:  $\pattern{\_}{\_}$ e simbol din signatura $\symb{\Sigma}$. de remarcat ca 
%$\pattern{\pattern{ \pi}{\psi}}{}$ este  pattern (not basic!) si pentru $\L$, tot dupa Def.~\ref{def:pattern}.}
In~\cite{ArusoaieLR2013SLE} we prove that the symbolic  transition system forward-simulates the concrete one, and that the concrete transition system backward-simulates the symbolic one. These two results then imply the naturally  expected properties of symbolic execution. In this paper we use symbolic execution  for the purpose of verifying RL formulas. 
%The next section briefly introduces Reachability Logic.
%
%\dl{La VMCAI sigur ne ataca (din nou) de ce nu utilizam conexiunea Galois sa relationa cele doua sisteme tranzitionale.}
%\vr{nu vad cum ne-ar putea ataca; aici doar pomenim de rezultatele  acelea (care s-ar putea formula ca si conexiuni Galois),  nu le folosim deloc.}

%\vspace*{-2ex}

\subsection{Reachability Logic}

\label{sec:dedsysrl}
We   recall  the syntax and semantics of a subset of reachability logic (RL)~\cite{rosu-stefanescu-2012-oopsla}. The formulas we consider are the  most commonly used ones for defining a language's semantics and for state properties about programs.
Then its proof system and togethter with the  soundness property~\cite{rosu-stefanescu-2012-oopsla} are briefly presented; these are essential in showing the correctness of our symbolic execution-based verification.

%\dl{Trebuie sa decidem daca scriem numai la prezent (e.g., we consider) sau viitor (we shall consider).}

%\vspace*{-4ex}


\subsubsection{Syntax and Semantics}
\label{sec:syntax}
We  consider the subset of reachability logic formulas that are pairs  $\varphi_1 \pmb{\Rightarrow} \varphi_2$, where the left and right-hand sides are disjunctions of patterns (cf.  Definition~\ref{def:pattern}) over a set of variables, say, $\Var$.
In particular, all semantical rules of a language are of this kind (cf.\ Definition~\ref{def:sem}).  
RL formulas can be  more general, as they may have conditions that are themselves RL formulas. However, we found the considered subset 
expressive enough for defining a language's semantics and for stating properties about programs.
% By abuse of notation we still call this subset  "Reachability Logic".



Semantically, a disjunction $\varphi \eqbydef \bigvee_{i\in I} \varphi_i$ of patterns is satisfied by  a configuration $\gamma$  and a valuation $\rho$,
written $(\gamma,\rho) \models \varphi$, if $(\gamma,\rho) \models \varphi_i$ for some $i \in I$. A configuration $\gamma$ 
is \emph{terminating} if there is no infinite
path in the transition system $(\T_\Cfg,\tran{}{\S})$ starting in $\gamma$, and  an RL formula  $\rrule{\varphi_1}{\varphi_2}{}$  is \emph{valid}, written $\S \models \varphi_1 \pmb{\Rightarrow} \varphi_2$, if for all terminating configurations $\gamma_1$ and valuations $\rho$ satisfying $(\gamma_1, \rho) \models  \varphi_1$,
 there is $\gamma_2$ such that $(\gamma_2, \rho) \models \varphi_2$ 
and $\gamma_1\ltran{*}{}{\S} \gamma_2$ in $(\T_{\Cfg},  \tran{}{\S})$. 

%\vspace*{-3.5ex}


\subsubsection{Proof System}
\label{sec:orig}
%\begin{figure}[t]
\begin{figure}{t}
%\vspace*{-8.5ex}
\begin{align*}
\textsf{[Axiom]}~  
&\dfrac{\rrule{\varphi}{\varphi'} \in \S
%\quad  \mathit{\phi \ patternless \ FOL \ formula} 
}
          {\S  \vdash_G \rrule{\varphi \pmb{\wedge} \phi}{\varphi'  \pmb{\wedge} \phi}}\\
\textsf{[Abstraction]}~  
& \dfrac{\S \vdash_G \rrule{\varphi}{\varphi'} \quad X \cap \var(\varphi') = \emptyset}
           {\S \vdash_G (\exists  X.\,\rrule{\varphi}{\varphi' })}\\                
\textsf{[Reflexivity]}~ 
&
\dfrac{\cdot}
          {\S \vdash \rrule{\varphi}{\varphi}}\\  
\textsf{[Consequence]}~ 
&
\dfrac{\models \varphi_i {\to} \varphi_{i+1}, i{\in}\{1,3\} ~~ \S \vdash_G \rrule{\varphi_2}{\varphi_3}}
          {\S \vdash_G \varphi_1 \pmb{\Rightarrow} \varphi_4}\\     
\textsf{[CaseAnalysis]}~          
& \dfrac{\S \vdash_G \rrule{\varphi_1}{\varphi} \quad \S \vdash_G  \rrule{\varphi_2}{\varphi}}
           {\S \vdash_G \rrule{(\varphi_1 \vee \varphi_2)}{\varphi}}\\
\textsf{[Transitivity]}~          
& \dfrac{\S \vdash_G \rrule{\varphi}{\varphi''} \quad (\S \cup G) \vdash \rrule{\varphi''}{\varphi'}}
           {\S \vdash_G \varphi \pmb{\Rightarrow} \varphi'}\\
\textsf{[Circularity]}~          
& \dfrac{\S \vdash_{G \cup\{ \rrule{\varphi}{\varphi'} \}}\rrule{\varphi}{\varphi'}}
           {\S \vdash_G\rrule{\varphi}{\varphi'}}
\end{align*}
%\vspace*{-4ex}
\caption{\label{fig:origrl}  Proof System for RL.}
%\vspace*{-4ex}
\end{figure}
%\end{figure}
We consider here the  version of the reachability logic proof system described in~\cite{rosu-stefanescu-2012-oopsla}. The proof system proves sequents of the form $\S \vdash_G \rrule{\varphi}{\varphi'}{}$ where $G$ is a set of formulas called \emph{circularities}. If $G=\emptyset$ then one  simply writes $\S\vdash\rrule{\varphi}{\varphi'}{}$.  The validity of a FOL formula $f$ is denoted $\models f$, and the  left and right-hand patterns of reachability-logic formulas are interpreted as FOL formulas~\cite{rosu-stefanescu-2012-oopsla}.
 $\varphi \pmb{\wedge} \phi$, for $\varphi \eqbydef \bigvee_{i \in I} \pi_i \pmb{\wedge} \phi_i$, is a shortcut for $\bigvee_{i \in I} \pi_i \pmb{\wedge} (\phi_i \wedge \phi)$.  

%The proof system is thus language-independent (parametric in the semantics).


\begin{definition}[weak well-definedness, \cite{rosu-stefanescu-2012-oopsla}]
\label{def:wwd}
A set of rules $\S$ is
\emph{weakly well-defined} if for each $\rrule{\varphi}{\varphi'} \in S$ and for all valuations  $\rho: \Var \to \T$ there exists  a configuration $\gamma$ such that $(\gamma,\rho) \models \varphi'$.
\end{definition}
%The main result regarding the proof system of RL that we shall be using is
\begin{proposition}[soundness, \cite{rosu-stefanescu-2012-oopsla}]
The deductive system of reachability logic is \emph{sound}: If $\S$ is weakly well-defined then $\S \vdash \varphi \pmb{\Rightarrow} \varphi'$ implies $\S \models \varphi \pmb{\Rightarrow} \varphi'$.
\end{proposition}
There is also a \emph{relative completeness} result, but we are not using it here.
Other results about the proof system, used in the sequel and proved in~\cite{rosu-stefanescu-2012-oopsla}, are:

%\vspace{-2ex}

\begin{itemize}
\item \emph{Substitution}:  $\S \vdash_G \theta(\varphi) \pmb{\Rightarrow} \theta(\varphi')$, if $\theta: \Var \to T_{\Sigma}(\Var)$ and $\S \vdash_G \varphi \pmb{\Rightarrow} \varphi'$;
\item \emph{Logical Framing}: $\S \vdash_G (\varphi  \wedge \phi)\!\pmb{\Rightarrow}\!(\varphi' \wedge \phi)$, if $\phi$ is a patternless FOL formula and  $\S \vdash_G \varphi \pmb{\Rightarrow} \varphi'$;
\item \emph{Set Circularity}: if $\S \vdash_G \varphi \pmb{\Rightarrow} \varphi'$ for each $\varphi \pmb{\Rightarrow} \varphi' \in G$ and $G$ is finite then
 $\S \vdash \varphi \pmb{\Rightarrow} \varphi'$ for each $\varphi \pmb{\Rightarrow} \varphi' \in G$;
 \item \emph{Implication}: if $\models \varphi \to \varphi'$ then $\S \vdash \varphi \pmb{\Rightarrow} \varphi'$;
  \item \emph{Monotony}:  if $\S\subseteq \S'$ then $\S \vdash \rrule{\varphi}{\varphi'}$ implies $\S' \vdash \rrule{\varphi}{\varphi'}$.
\end{itemize}

%\vspace{-2ex}


The proof system in Figure~\ref{fig:origrl} leaves a lot of freedom to the user as to which rule to apply when verifying programs. 
At any step of the proof, one must choose, whether to include the current goal in the circularities $G$, i.e., to apply the \textsf{Circularity} rule; or to derive some intermediate goal $\varphi''$ using the  \textsf{Transitivity} rule, and to continue from there on by using the current set of circularities as new semantical rules; or to split the premise of the current goal into two formulas
using the \textsf{CaseAnalysis} rule, which, thanks to the \textsf{Consequence} rule, can be arbitrary, provided their disjunction
is logically equivalent to the premise. 


%\vspace{-1ex}

\section{Symbolic Execution for Reachability-Logic Verification}
\label{sec:serlv}


We show in this section how symbolic execution can be used for verifying RL formulas in a systematic manner.  We show that, under the hypothesis of a \emph{total} semantics, which amounts to saying that all situations are "covered" by the semantical rules, the tree generated by symbolic execution constitutes an (abbreviated) proof tree for a RL formula. The \textsf{Circularity} rule of symbolic execution, which allows one to prove programs with possibly  unbounded loops by reusing goals to be proved  as hypotheses, is here replaced by an instance of the Circularity Principle~\cite{rosu-lucanu-2009-calco} for RL formulas. Using this principle amounts to performing
symbolic execution in an extended semantics which includes the goals as new semantical rules. A goal can only be used in the symbolic
execution of a given pattern only when it "covers" the pattern, which means that all symbolic successors of the pattern are computed 
by applying the goal as a rewrite rule.
The following lemma characterises  transitions in the symbolic transition system.
\begin{lemma}[Symbolic Transitions]
\label{lem:dedsymbex}
For each transition $\varphi \ltran{\symb{\alpha}}{}{}   \varphi'$ in the symbolic transition system, with $\varphi \eqbydef \pattern{\pi}{\phi}$ and $\alpha \eqbydef \rrule{\pattern{\pi_l}{{\phi_l}} }{\pattern{\pi_r}{\phi_r}} \in \S$, there exists a substitution $\sigma$ such that $\varphi=\pattern{\sigma(\pi_l)}{\phi}$ and  $\varphi' = \pattern{\sigma(\pi_r)}{(\phi \wedge \sigma(\phi_l) \wedge \sigma(\phi_r))}$.
\end{lemma}
%\begin{proof}
%Since $\alpha \eqbydef \rrule{\pattern{\pi_l}{{\phi_l}} }{\pattern{\pi_r}{\phi_r}}$, the corresponding symbolic rule $\symb{\alpha}$
%is of the form~(\ref{eq:transform}), i.e, $\symb{\alpha} = (\rrule{\pattern{\pi_l} {\psi}}{\pattern{\pi_r}{(\psi \wedge \phi_l \wedge \phi_r)}})$ where $\psi$
%is a fresh Boolean variable. The transition  $\varphi \ltran{\symb{\alpha}}{}{}   \varphi'$ is obtained by rewriting $\varphi \eqbydef \pattern{\pi}{\phi}$
%with $\symb{\alpha}$, hence, there is a substitution $\sigma \cup {(\psi \to \phi)}$ such that $(\sigma \cup (\psi \to \phi)) (\pattern{\pi_l}{\psi}) = \pattern{\pi}{\phi}$
%and  $\varphi' = (\sigma \cup (\psi \to \phi))(\pattern{\pi_r}{(\psi \wedge \phi_l \wedge \phi_r)})$. The conclusion of the lemma is obtained by applying the substitution 
%$\sigma \cup (\psi \to \phi)$ in the last two  identities. \hfill $\Box$
%\end{proof}



%We are interested in verifying RL formulas of the form $\pattern{\symb{\pi}}{\symb{\phi}} \pmb{\Ra} \pattern{\symb{\pi'}}{\symb{\phi'}}$, where $\pattern{\symb{\pi}}{\symb{\phi}}, \pattern{\symb{\pi'}}{\symb{\phi'}}$
%are patterns over $\symb{V}$. Note that  the transitions ${\pattern{\symb{\pi}}{\symb{\phi}}}\ltran{\symb{\alpha}}{}{}{\pattern{\symb{\pi'}}{\symb{\phi'}}}$ in the symbolic transitions system can be seen as RL formulas. In order to ease the reading,  in this section we write RL formulas representing symbolic transitions without mentioning the superscript $\symb{}$. We may also write, e.g., $\varphi\ltran{\symb{\alpha}}{}{}\varphi'$ whenever $\symb{\varphi}\ltran{\symb{\alpha}}{}{}\symb{\varphi'}$, where $\symb{\varphi}$ (resp. $\symb{\varphi'}$) is obtained from $\varphi$ (resp. $\varphi'$) by replacing each  variable from $\Var$ with a distinct variable from $\symb{V}$.
% Therefore is meaningful to write $\S\models {\pattern{\symb{\pi}}{\symb{\phi}}}\ltran{\symb{\alpha}}{}{}{\pattern{\symb{\pi'}}{\symb{\phi'}}}$ .

%\vr{de spus ceva aici despre faptul ca faptul ca avem patternuri peste $\symb{V}$ nu este esential pentru abordare, fiindca numele variabilelor este ne-esential; $\symb{V}$ doar face legatura intre executia simbolica si RL. Prin urmare, in restul articolului eliminam subscriptul $\symb{}$, pentru a simplifica notatiile.}

%\dl{
%%\begin{remark}
%%$\symb{V}$ is a set o variables, hence the transitions ${\pattern{\symb{\pi}}{\symb{\phi}}}\ltran{*}{}{}{\pattern{\symb{\pi'}}{\symb{\phi'}}}$ in the symbolic transitions system can be seen as RL formulas. Therefore is meaningful to write $\S\models {\pattern{\symb{\pi}}{\symb{\phi}}}\ltran{\symb{\alpha}}{}{}{\pattern{\symb{\pi'}}{\symb{\phi'}}}$ or $\S\models {\pattern{\symb{\pi}}{\symb{\phi}}}\ltran{*}{}{}{\pattern{\symb{\pi'}}{\symb{\phi'}}}$.
%%In order to ease the reading,  in this section we write RL formulas representing symbolic transitions without mentioning the superscript $\symb{}$. 
%We may go further with this interplaying between formulas and patterns and write, e.g., $\varphi\ltran{\symb{\alpha}}{}{}\varphi'$ whenever $\symb{\varphi}\ltran{\symb{\alpha}}{}{}\symb{\varphi'}$, where $\symb(\varphi)$ (resp. $\symb(\varphi')$ is obtained from $\varphi$ (resp. $\varphi'$) by replacing each its variable from $\Var$ with a distinct variable from $\symb{V}$.
%%\end{remark}
%}

%\dl{Va trebuie sa justificam introducerea tuturor notiunilor de mai jos; asa cum e acum, prezentarea e cam seaca si cititorul nu stie incotro vrem sa mergem. Eu am adaugat veva dar trebuie revizuit si completat.}
\subsection{Derivatives, Total Semantics, and Cover}
The symbolic transition system  $(\symb{\T}_{\symb{\Cfg}},\tran{}{\symb{\S}})$ is 
useful for defining some notions that we use in the verification of reachability-logic formulas.
A first, essential notion is that of \emph{derivative} of an elementary pattern $\varphi$, which is is the disjunction of all elementary patterns that are targets of
symbolic transitions starting in $\varphi$.

%\vspace{-0.6ex}

\begin{definition}[Derivative]
\label{def:deriv}
For a set of semantical rules $\S$ and an elementary pattern $\varphi $, its \emph{derivative} is defined by   $\Delta_\S(\varphi) \eqbydef \bigvee_{\alpha \in \S, \varphi \ltran{\symb{\alpha}}{}{}   \varphi'} \varphi'$.
\end{definition}
%\vspace{-0.66ex}
We note that if $\S$ is finite then $\Delta_\S(\varphi)$ is a finite disjunction because symbolic transition systems are \emph{finitely branching}.
Note that according to the Definition~\ref{def:deriv}, the derivative of a pattern $\varphi$ can be $\false$ (i.e., the empty disjunction).
%\vspace{-0.5ex}
 \begin{definition}[Derivable Pattern]
  An elementary pattern $\varphi \eqbydef \pattern{\pi}{\phi}$ is \emph{derivable} for $\S$  if $\Delta_\S(\varphi)$ is a nonempty disjunction.
 \end{definition}
The following notion of \emph{total} semantics is essential for the soundness of RL-formula verification by symbolic execution. An example showing that  the absence of totality leads to unsoundness was given in the introduction of the paper.
%\vspace{-0.6ex}
 \begin{definition}[Total Semantics]
 \label{def:total}
 We say that a set $\S$ of semantical rules is \emph{total} if for each basic pattern $\pi$ occurring in the left-hand side of a rule,
 the disjunction $\bigvee_{(\pi \wedge \phi \pmb{\Ra} \varphi)\in \S} \phi$ is valid in FOL.
 \end{definition}
 %\vspace{-0.7ex}
 \begin{remark}
\label{rem:impnottotal}
The semantics of \IMP is not total because of the rules for division (and modulo):
$\rrule{\pattern{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1\terminal{/}I_2}}}{I_2\not=_\mathit{Int}0}}
{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1/_{\mathit{Int}}I_2}}}$, whose  left-hand side pattern
$\kprefix[black]{cfg}{\kprefix[black]{k}{I_1/_{\!\mathit{Int}}I_2}}$ does not meet the condition of Definition~\ref{def:total}.
 The semantics can be made total by adding a rule
$\rrule{\pattern{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1\terminal{/}I_2}}}{I_2=_\mathit{Int}0}}
{\kall[black]{cfg}{\mathit{error}}}$ that leads divisions by zero into ``error'' configurations. We assume hereafter that the semantics of \IMP has been transformed into a total semantics.
%One may think of a total semantics as one that throws exceptions for  partial definitions.
\end{remark}

%\vspace{-1.5ex}
 
\begin{remark} 
\label{rem:substunique}
For  basic patterns  $\pi,\pi'$,   let $\sigma^\pi_{\pi'}$ be a substitution such that $\sigma^\pi_{\pi'}(\pi') =\pi$.
Since $=$ is   syntactical equality, the substitution $\sigma^\pi_{\pi'}$ is unique if it exists.
\end{remark}
The notion of cover, defined below, is also essential  for the soundness of  RL-formula verification by symbolic execution, in particular, when a proof goal is circularly used as a hypothesis, which amounts to  performing symbolic execution using the goal as a new semantical rule. Such  goals can only  be used in symbolic execution only when they  \emph{cover} the pattern being symbolically executed:

%\vspace{-0.6ex}

\begin{definition}[Cover]
\label{def:cover}
Consider an elementary pattern $\varphi \eqbydef \pi \wedge \phi$. 
A set of rules  $\S'$ 
satisfying $\models \phi \to \bigvee_{\alpha  \eqbydef (\rrule{\pattern{\pi_\alpha}{\phi_\alpha}}{\varphi_\alpha}) \in \S'} \sigma^\pi_{\pi_\alpha}(\phi_\alpha)$
is called a \emph{cover} of $\varphi$.
\end{definition}
%\vspace{-0.6ex}
Note that if $\S'$ is a cover for $\varphi \eqbydef \pi \wedge \phi $, the disjunction $ \bigvee_{\alpha  \eqbydef (\rrule{\pattern{\pi_\alpha}{\phi_\alpha}}{\varphi_\alpha}) \in \S'} \sigma^\pi_{\pi_\alpha}(\phi_\alpha)$ is nonempty, otherwise the validity $\models$ in Definition~\ref{def:cover} would not hold (since an empty disjunction 
is $\false$). In particular, there is at least one rule in $\S'$  that matches $\pi$, and, as a consequence, the derivative $\Delta_\S'(\varphi)$ is a nonempty disjunction.
The next result exhibits a simple and useful example of the notion of cover.

%\vspace{-0.5ex}


\begin{lemma}
\label{obs:totalcov}
If $\S$ is total and $\varphi$ is derivable for $\S$ then $\S$ is a cover for~$\varphi$.  
\end{lemma}

%\vspace{-0.5ex}


\noindent Using the notion of cover we obtain a new derived rule of the RL proof system:
%\vspace{-0.5ex}

\begin{theorem}
\label{lem:deriv}
If $\S'\subseteq \S$  is a cover for $\varphi$, then $\S \vdash_G \varphi \pmb{\Rightarrow} \Delta_{\S'}(\varphi)$ for any set $G$.
\end{theorem}
%\vspace{-0.5ex}

\begin{corollary}
\label{cor:symbexec}
If $\S$  is total and $\varphi$ is derivable for $\S$, then $\S \vdash \varphi \pmb{\Rightarrow} \Delta_{\S}(\varphi)$.
\end{corollary}
%\begin{proof}
%Use Theorem~\ref{lem:deriv} with $\S' = \S$ and $G = \emptyset$, and Lemma~\ref{obs:totalcov}.
%\end{proof}



\subsection{Weakly Well-Definable Semantics}

%\vspace{-1ex}


Before we can use the soundness of the RL deductive system we need to deal with the issue that operational semantics are not
always weakly well-defined (Def.~\ref{def:wwd}) as required by the RL soundness result. For example, the semantics of \IMP is not weakly well-defined
due to the rules for division and modulo, which,  for valuations
$\rho$ mapping divisors to $0$, have no instance of their right-hand side. 
%\dl{Poate ar trebui sa consideram regula cu $\%$ in loc de impartire daca ramanem la exemplul cu gcd.}

However, due to the introduction of the rule $\rrule{\pattern{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1\terminal{\%}I_2}}}{I_2=_\mathit{Int}0}}
{\kall[black]{cfg}{\mathit{error}}}$ in order to make the semantics total (cf.~Remark~\ref{rem:impnottotal}),
the semantical of division can now equivalently rewritten using just one (reachability-logic) rule:
\noindent 
\begin{equation}
\small
\label{eq:divwwd}
\rrule{\pattern{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1\terminal{\%}I_2}}}{I_2 \not =_{Int} 0}}
{(\pattern{\kprefix[black]{cfg}{\kprefix[black]{k}{I_1\%_{\mathit{Int}}I_2 }}}{ I_2  =_{Int} 0}) \vee (\kall[black]{cfg}{error})}
\end{equation}
\noindent By using this rule instead of the two original ones, and by applying the same transformation for the rules defining division, the semantics becomes weakly well-defined. This transformation
is formalised as follows.

\begin{definition}[$\S^\Delta$]
\label{def:sdelta}
Given a set of semantical rules $\S$, the set of semantical rules $\mathbf{\S^\Delta}$ is defined 
by  $\S^\Delta \eqbydef \{ \rrule{\pi}{\Delta_{\S}(\pi)}{} \mid  (\rrule{\pi \wedge \phi}{\varphi}{}) \in \S \}$.
\end{definition}


%
%\vr{conditia \emph{weak-well-definedness}  era abstracta (folosea derivative, etc) si nu-mi era foarte clar ce  implica asupra regulilor. 
%Propun definitia alternativa mai simpla:}
%
%\begin{definition}[Weakly Well-Definable Semantics]
%We say that a set of semantical rules $\S$ is \emph{weakly well-definable} if
%\begin{itemize}
%\item all the rules $\varphi \pmb{\Ra} \varphi' \in S$ are valid RL formulas: $\S \models \varphi \pmb{\Ra} \varphi'$;
%\item for all rules $\varphi \pmb{\Ra} \varphi' \in S$ with $\varphi \eqbydef \pi \wedge \phi$, and all $\rho : \Var \to \T$,
%$\rho(\pi) \in \T$.
%\end{itemize}
%\end{definition}

%\vspace{-2ex}

\begin{definition}[Weakly Well-Definable Semantics]
\label{def:wwdf}
We say that a set of semantical rules $\S$ is \emph{weakly well-definable} if $\S^\Delta$ is weakly  well-defined. 
\end{definition}
If a semantics $\S$ is not weakly well-defined, but only weaky well-definable (which happens quite often - e.g., all the languages defined  in the \K framework 
that have rules for numeric division are in this case) then one can use the $\S^\Delta$ semantics, which is by definition  weakly well-defined and ensures
soundness of the RL deduction system. We note that in this case $\S^\Delta$ is also (trivially) total, which is  required by the soundness of our approach as shown in the example in the introduction.
%Weak well-definability of a semantics is, like totality,  an essential condition for soundness of RL-formula verification using symbolic execution. Actually, we prove below weak well-definability
%implies totality, hence, it is the only  condition we shall require from a language's semantics in order to apply our approach:
%\begin{lemma}
%\label{lem:wwdimpliestotal}
%If $\S$ is well-definable then $\S$ is total.
%\end{lemma}
%\begin{proof}
%We assume without restriction of generality that for each basic pattern $\pi$ occurring in the left-hand side of some rule $\alpha \in \S$,
%there is no pattern $\pi'$ occurring in some other rule in $\alpha' \in \S$ such that $\pi$ is an instance of $\pi'$ (i.e., $\pi$  is obtained from $\pi'$ by a substitution).
%If such $\pi'$ exist then the rule $\alpha'$ can always be modified to "include" the rule $\alpha$  and the  rule $\alpha$ can be removed from $\S$.
%
%Hence, any rule in $\S$ that matches $\pi$ matches it with the identity substitution.
%
%Consider then any basic pattern $\pi$ occurring in the left-hand side of some rule in $\S$, and the corresponding rule $( \rrule{\pi}{\Delta_{\S}(\pi)}{}) \in \S^\Delta$. Using Lemma~\ref{lem:dedsymbex} and Definition~\ref{def:deriv} of derivatives, as well as the above observation, 
%$\Delta_\S(\pi) = \bigvee_{(\rrule{\pattern{\pi}{\phi_l}}{\pattern{\pi_r}{\phi_r}}) \in \S}(\pattern{\pi_r}{(\phi_l \wedge \phi_r}))$. 
%Since $\S$ is weakly well-definable, the right-hand side $\Delta_\S(\pi)$ of the rule $( \rrule{\pi}{\Delta_{\S}(\pi)}{}) \in \D^\Delta$ satisfies the property
%\textit{for any $\rho : \Var \to \T$ there exists $\gamma \in \T^\Cfg$ such that $\gamma = \rho(\Delta_\S(\pi))$}. Given the above definition of $\Delta_\S(\pi)$,
%this implies that for each $\rho : \Var \to \T$, there exists $(\rrule{\pattern{\pi}{\phi_l}}{\pattern{\pi_r}{\phi_r}}) \in \S$ such that $\rho(\phi_l \wedge \phi_r) = \true$,
%which implies $\rho(\phi_l) = \true$. Thus, for each $\rho : \Var \to \T$, $\rho(\bigvee_{(\rrule{\pattern{\pi}{\phi_l}}{\pattern{\pi_r}{\phi_r}}) \in \S} \phi_l) = \true$,
%which is equivalent to $\models \bigvee_{(\rrule{\pattern{\pi}{\phi_l}}{\pattern{\pi_r}{\phi_r}}) \in \S} \phi_l$, which is just the totality condition for $\pi$. 
%
%Since 
%the basic pattern $\pi$ occurring in the left-hand side of some rule $\alpha \in \S$ was chosen arbitrarily we obtain the totality condition for $\S$. 
%\end{proof}
 A few other useful properties of the $\S^\Delta$ construction  are given below.
%\vspace{-2ex}
\begin{lemma}
\label{lem:sdeltaequivs}
$\S \models \varphi \pmb{\Ra} \varphi'$ iff $\S^\Delta \models \varphi \pmb{\Ra} \varphi'$.
\end{lemma}
%\begin{proof}
%$(\Rightarrow)$ From $\S \models \varphi \pmb{\Ra} \varphi'$ we obtain that for each terminating configuration $\gamma \in \T$ and valuation $\rho$
%such that $(\gamma,\rho) \models \varphi$, there is $\gamma' \in \T$ and a path $\gamma \ltran{\alpha^*}{}{\S} \gamma'$, with $\alpha^* \in \S^*$,  such that $(\gamma',\rho)  \models \varphi'$. We prove by induction on the length of the sequence $\alpha^*$ that $(\spadesuit)$: $\gamma \ltran{\alpha^*}{}{\S} \gamma'$, which implies  the direct $(\Rightarrow)$ implication.
%
%The base case of $(\spadesuit)$ is trivial. For the inductive step, we use the fact that each transition $\gamma_1  \ltran{\alpha}{}{\S} \gamma_2$
%is induced by semantical rule $\alpha \eqbydef \rrule{\pattern{\pi}{\phi}}{\varphi}\in \S$ with a valuation $\rho$. Then, the corresponding rule $\rrule{\pi}{\Delta_\S(\pi)} \in \S^\Delta$ induces a corresponding  transition $\gamma_1  \ltran{\alpha}{}{\S^\Delta} \gamma_2$ with the same valuation $\rho$.
%
%$(\Leftarrow)$ By analogy with the direct implication. The only difference  is in the inductive step:  each transition $\gamma_1  \ltran{\alpha}{}{\S^\Delta} \gamma_2$
%is induced by semantical rule $\alpha^{\Delta} \eqbydef \rrule{\pi}{\Delta_\S(\pi)}{} \in \S^\Delta$ with a valuation $\rho$. Then, the rule $ \alpha \eqbydef \rrule{\pattern{\pi}{\phi}}{\varphi}\in \S$ induces a corresponding  transition $\gamma_1  \ltran{\alpha}{}{\S} \gamma_2$ with the same valuation $\rho$. \hfill  $\Box$
%
%\end{proof}
%\vspace{-2ex}
\begin{lemma}
\label{lem:derivsdelta}
A pattern $\varphi$ is derivable for $\S$ if and only if $\varphi$ is derivable for $\S^{\Delta}$.
\end{lemma}
%\begin{proof}
%By definition, $\varphi \eqbydef \pattern{\pi}{\phi}$ is derivable for $\S$ means that $\Delta_\S(\varphi)$ is not the empty disjunction. This holds if and only if there exists 
%a rule $\rrule{\pattern{\pi_l}{\phi_l}}{ \pattern{\pi_r}{\phi_r}} \in\S $ such that $\pi_l$ matches $\pi$. The proof is finished by noting that $\pi_l$ is also the left-hand side of the rule corresponding $\rrule{\pi_l}{\Delta_\S(\pi_l)} \in \S^\Delta$. \hfill $\Box$
%\end{proof}
%\begin{lemma}
%If $\S$ is weakly well-definable then $\S$ is total.
%\end{lemma}


%
%\begin{remark}
%Applying rules in  $\S^\Delta$ on patterns amounts to applying rules of the form $(\ref{eq:transform})$ on symbolic configurations, which 
%is what our implementation of symbolic execution does. Thus, our implementation  can equivalently be expressed as  applying the $\S^\Delta$ semantics on patterns. We exploit this analogy for showing that our implementation is sound for proving reachability-logic formulas.
%\end{remark}

%\vspace{-3ex}

\subsection{Reachability-Logic Verification by Symbolic Execution}
\label{sec:soundimpl}

%\vspace{-1ex}

 Assume a language with a  semantics $\S$, and a finite of RL formulas with elementary patterns in their left-hand sides, say,  $G =\{\varphi_i \pmb{\Rightarrow} \varphi'_i \mid i = 1, \ldots, n\}$.  We now have almost all ingredients for proving $\S \models G$ by symbolic execution. 
 
 \begin{definition}
A RL formula $\rrule{\varphi}{\varphi'}$ is \emph{derivable} for $\S$ if the left-hand side $\varphi$ is derivable for $\S$.
 If $G$ is a set of RL formulas, then ${\Delta_{\S}(G)}$ denotes the set $\{\rrule{\Delta_\S(\varphi)}{\varphi'}\mid \rrule{\varphi}{\varphi'} \in G\}$.  If $\Phi$ is a set of RL formulas, then $\S \vdash \Phi$ denotes the conjunction $\bigwedge_{\varphi \pmb{\Rightarrow} \varphi' \in \Phi} \S \vdash \varphi \pmb{\Rightarrow} \varphi'$,
and  $\S \models \Phi$ denotes $\bigwedge_{\varphi \pmb{\Rightarrow} \varphi' \in \Phi} \S \models \varphi \pmb{\Rightarrow} \varphi'$.  
\end{definition}
%We assume that all the goals in $G$ are derivable for $\S$.
The last result we shall be using   in order to prove $S \models G$  by symbolic execution  says  the formulas $G$ themselves may be used   as (circular) hypotheses:
 
\begin{theorem}[Circularity Principle for RL]
\label{th:rlsymbex}
If $\S$ is total and weakly well-defined, and $G$ is derivable for $\S$, then $\S \cup G \vdash \Delta_\S(G)$ implies $\S \models G$.
\end{theorem}
%\begin{proof}
%For all $i = 1,\ldots, n$ we  apply the
%\textsf{[Transitivity]} rule with $\varphi''_i \eqbydef \Delta_\S(\varphi_i)$, and obtain:
%$$\dfrac{\S \vdash_G \varphi_i \Rightarrow \Delta_\S(\varphi_i) \quad (\S \cup G) \vdash \Delta_\S(\varphi_i)  \Rightarrow \varphi'_i}{\S \vdash_G \varphi_i \Rightarrow \varphi'_i}$$
%The first hypothesis: $S \vdash_G \varphi_i \Rightarrow \Delta_\S(\varphi_i)$  holds thanks to Theorem~\ref{lem:deriv} and Lemma~\ref{obs:totalcov}.
% The second one, $(\S \cup G) \vdash \Delta_\S(\varphi_i)  \Rightarrow \varphi'_i$ is a hypothesis of the theorem. Hence, we obtain $S \vdash_G \varphi_i \Rightarrow \varphi'_i$ for all $i = 1,\ldots, n$, i.e., 
%$S \vdash_G G$.
% Then we obtain 
%$S \vdash G$ by applying the derived rule \emph{Set Circularity} of RL
%Finally, the soundness of $\vdash$ (with $\S$ weakly well defined) implies $\S \models G$.
%
%\end{proof}
If a semantics $\S$ is not weakly well-defined but only weakly-well definable, one can use 
Theorem~\ref{th:rlsymbex} with $\S^\Delta$ instead of $\S$, and, under the same hypotheses regarding the derivability of $G$, 
one can deduce $\S \models G$, thanks to  Lemmas~\ref{lem:sdeltaequivs} and~\ref{lem:derivsdelta}.



Theorems~\ref{lem:deriv} and~\ref{th:rlsymbex}  
 together with the soundness  of the derived deduction rules of RL mentioned in Section~\ref{sec:dedsysrl} constitute  the formal basis for the soundness of our implementation of verification of RL formulas based on symbolic execution.

This verification amounts to searching proofs for $\S \cup G \vdash  \Delta_{\S}(G)$.
An important observation is that we do not need to use the \textsf{Circularity} rule of the  RL proof system (Figure~\ref{fig:origrl}) because we give all circularities $G$ right from the  beginning in the Circularity Principle.
 So, the difficult and tricky task of detecting circularities during the proof process is avoided. 
It could be claimed that finding an adequate set of the circularities $G$, allowing the Circular Principle to be used for proving $\S \models G$, is as difficult as the finding them during the proving process. This is only true in theory: in practice,  the main advantage of our approach is that it is   automatic and it can be tried on several guesses for the set~$G$. Moreover, when a proof fails,  one may check the path conditions returned by symbolic execution to guess what new goals should be added for progressing in the proof.
\begin{figure}[t]
%\begin{figure}[t]
%\vspace*{-5ex}
\begin{align*} 
\textsf{[SymbolicStep]}~
&\dfrac{\varphi \ \mathit{derivable \ for} \ \S}{\S \cup G\vdash \varphi  \pmb{\Rightarrow} \Delta_{\S}(\varphi)}\\  
\textsf{[CircularHypothesis]}~
&\dfrac{\alpha \in G  \quad \alpha \ \mathit{covers} \ \varphi}{\S \cup G\vdash \varphi  \pmb{\Rightarrow} \Delta_{\{\alpha\}}(\varphi)}\\ 
\textsf{[Implication]}~
&\dfrac{\models \varphi \to \varphi' }
          {\S \cup G\vdash \varphi \pmb{\Rightarrow} \varphi'}\\     
\textsf{[CaseAnalysis]}~          
& \dfrac{\S \cup G\vdash \varphi_1 \pmb{\Rightarrow} \varphi \quad \S \cup G \vdash  \varphi_2 \pmb{\Rightarrow} \varphi}{\S\cup G \vdash (\varphi_1 \vee \varphi_2) \pmb{\Rightarrow} \varphi}\\
\textsf{[Transitivity]}~          
& \dfrac{\S \cup G\vdash \varphi \pmb{\Rightarrow} \varphi'' \quad \S \cup G\vdash \varphi'' \pmb{\Rightarrow} \varphi'}{\S \cup G \vdash \varphi \pmb{\Rightarrow} \varphi'}
\end{align*}
%\vspace*{-2ex}
\caption{\label{fig:altrl} \mbox{Proof System for~$\S \cup G \vdash \Delta_\S(G)$.}}
%\end{figure}
\end{figure}
%\vr{pentru sistemul din Fig. 6 poate ar trebui sa folosim un alt simbol de entailment.}

We search for proofs of $\S \cup G \vdash \Delta_\S(G)$ in the deductive system from Figure~\ref{fig:altrl}, which is a subsystem of the RL proof system. This is because
all its rules are either deductive rules of RL (like \textsf{Transitivity} and \textsf{CaseAnalysis}) or derived rules, like \textsf{Implication}. 
\textsf{SymbolicStep} is a also derived rule, which is shown using  $\S \cup G\vdash \varphi  \pmb{\Rightarrow} \Delta_{\S}(\varphi)$ (cf.~Corollary~\ref{cor:symbexec}) and the \emph{Monotony} 
derived rule of RL.  Finally, \textsf{CircularHypothesis} is also a derived rule thanks to Theorem~\ref{lem:deriv}.

\begin{example}
\label{ex:gcdproof}
We show how the RL formula~(\ref{eq:specgcd}) is proved using the deductive system in Figure~\ref{fig:altrl}, which amounts to verifying the \texttt{gcd} program.
For this, we consider the two following additional formulas, where \texttt{while} denotes the program fragment consisting of the \texttt{while} loop, and \texttt{body}
denotes the body of the loop:
\begin{eqnarray}
&&\!\!\!\!{\pattern{\kall[black]{\mathrm{cfg}}{\kall[black]{k}{\mathtt{while}}\kall[black]{env}{\texttt{a}{\mapsto}a\;\texttt{b}{\mapsto}b\;\texttt{x}{\mapsto}x\;\texttt{y}{\mapsto}y\;\texttt{r}{\mapsto}r}}\!}{\!\mathit{gcd}(a,b)\!=\!\mathit{gcd}(x,y)\!\wedge \!x\!\geq\!0\!\wedge\!y\!\geq\!0}} \pmb{\Ra}\nonumber \\
&&\!\!\!\!{\pattern{\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\texttt{a}{\mapsto}a\;\texttt{b}{\mapsto}b\;\texttt{x}{\mapsto}x'\;\texttt{y}{\mapsto}y'\;\texttt{r}{\mapsto}r'}}}{\mathit{gcd}(a,b)\!=\!\mathit{gcd}(x',y')\!\wedge \!x'\!\geq\!0\!\wedge\!y'\!=\!0}}\label{eq:specgcd2}\\
&&\!\!\!\!{\pattern{\kall[black]{\mathrm{cfg}}{\kprefix[black]{k}{\mathtt{body}}\kall[black]{env}{\texttt{a}{\mapsto}a\;\texttt{b}{\mapsto}b\;\texttt{x}{\mapsto}x\;\texttt{y}{\mapsto}y\;\texttt{r}{\mapsto}r}}\!}{\!\mathit{gcd}(a,b)\!=\!\mathit{gcd}(x,y)\!\wedge \!x\!>\!0\!\wedge\!y\!\geq\!0}}~\pmb{\Ra}\nonumber \\
&&\!\!\!\!{\pattern{\kall[black]{cfg}{\kall[black]{k}{\kdot}\kall[black]{env}{\texttt{a}{\mapsto}a\;\texttt{b}{\mapsto}b\;\texttt{x}{\mapsto}x'\;\texttt{y}{\mapsto}y'\;\texttt{r}{\mapsto}r'}}}{\mathit{gcd}(a,b)\!=\!\mathit{gcd}(x',y')\!\wedge \!x'\!\geq\!0\!\wedge\!y'\!\geq\!0}~~}\label{eq:specgcd3}
\end{eqnarray}
The rules say that the  \texttt{while} loop and  its body preserve an invariant: the $\mathit{gcd}$ of the values of
\texttt{a}, \texttt{b} equals the $\mathit{gcd}$ of the values of \texttt{x}, \texttt{y}. There are  pre and post-conditions on these values, with slight
differences between the two rules.  

We consider the set of goals $G$ consisting of the formulas~(\ref{eq:specgcd}), (\ref{eq:specgcd2}), and~(\ref{eq:specgcd3}),
and 	apply the deductive system in Figure~\ref{fig:altrl} to these goals in order to prove them:
\begin{itemize}
\item the formula~(\ref{eq:specgcd}) is proved by applying a number of times the~\textsf{SymbolicStep} rule until the \textsf{k} cell contains the 
 \texttt{while} program fragment. Then, the~\textsf{CircularHypothesis} rule is applied with the formula~(\ref{eq:specgcd2}). Next, the~\textsf{Implication} rule
 is used to prove that the pattern resulting from applying the  formula~(\ref{eq:specgcd2}) implies the right-hand side of the formula~(\ref{eq:specgcd}). Finally, the
 \textsf{Transitivity} rule builds a  proof of~(\ref{eq:specgcd}) from the individual rule applications  described above. 
 \item the formula~(\ref{eq:specgcd2}) is proved by applying a number of times the~\textsf{SymbolicStep} and~\textsf{CaseAnalysis} rules, until the program remaining to be executed is either:
 \begin{itemize}
 \item the empty program: then, the~\textsf{Implication} rule
 is used to prove that the current pattern implies the right-hand side of the formula~(\ref{eq:specgcd2}), and then
 \textsf{Transitivity}  builds a  proof of~(\ref{eq:specgcd2}) from these individual rule applications;
 \item the \texttt{body} program (i.e the loop's body), possibly followed by some other program (as denoted by the dots in the \textsf{k} cell).
 In this case, \textsf{CircularHypothesis}  is applied with the formula~(\ref{eq:specgcd3}), then \textsf{Implication} 
 is used to prove that the current pattern implies the right-hand side of the formula~(\ref{eq:specgcd2}), and finally
 \textsf{Transitivity} builds a  proof of~(\ref{eq:specgcd2}) from these  rule applications.
 \item the formula~(\ref{eq:specgcd3}) is proved  by applying a number of times the~\textsf{SymbolicStep} rule until the \textsf{k} cell contains the 
 \texttt{while} program fragment once again. From this point on, the proof is completely similar to the proof of~(\ref{eq:specgcd}).
 \end{itemize}
\end{itemize}
This concludes the proof of  the set of goals~(\ref{eq:specgcd}), (\ref{eq:specgcd2}), and~(\ref{eq:specgcd3}), and, in particular,
of the fact that the \texttt{gcd} program meets its specification~(\ref{eq:specgcd}). Note how the proofs of all goals used symbolic execution as well  other goals as circular hypotheses.
%\dl{Cred ca ar trebui sa reamintim ca semantica lui IMP este transformata in una totala.}
%\vr{done, cf Remark 3 la sfarsit}
\end{example}

%\vr{de insistat pe faptul ca tool-ul nostru genereaza un arbore  de demonstratie in sistemul deductiv din Fig.~\ref{fig:altrl}, care este un un subsistem al  celui de la RL.}
%
%Our tool works as follows: \ldots
%\dl{Partea care urmeaza o vom scrie dupa ce avem toolul.}


%first, it computes the set of goals $G' \eqbydef \Delta_{\S}(G)$. Then, it searches for proofs of $\S \cup G \vdash  G'$ by building a proof tree, whose nodes are sets of patterns. The root consists of  all the left-hand sides of all goals in~$G'$. The proof is built by  choosing a pattern $\varphi$ in the current node
%and by applying:
%\begin{itemize}
%\item \emph{symbolic execution with $\S$}: if $\varphi$ is derivable for $\S$, but no goal in $G$ is a cover for $\varphi$, 
%we generate a new node in which   $\varphi$ is replaced by the set of elementary patterns whose disjunction is $\Delta_{\S}(\varphi)$. This amounts to applying the \emph{symbolic execution} derived rule $\S \cup G \vdash \varphi \Ra \Delta_{\S}(\varphi)$,  which  holds by Theorem~\ref{lem:deriv} and Lemma~\ref{obs:totalcov} ($\S$ being total, it is a cover for $\varphi$, cf.\ Lemma~\ref{obs:totalcov}). The \textsf{[CaseAnalysis]}
%rule  of RL was also implicitly used for decomposing  $\Delta_{\S}(\varphi)$ into its disjuncts.
%
%\item \emph{symbolic execution with  $G$}: if  a goal in $\alpha \in G$ is a cover for $\varphi$ then we generate a new node in which   $\varphi$ is replaced by the set of elementary patterns whose disjunction is $\Delta_{\{\alpha\}}(\varphi)$.  This amounts to
%applying the
%\emph{symbolic execution} derived rule $\S \cup G \vdash \varphi \Ra \Delta_{\{\alpha\}}(\varphi)$, which is sound by Theorem~\ref{lem:deriv}. Again, the \textsf{[CaseAnalysis]}
%rule  of RL was  used for breaking $ \Delta_{\{\alpha\}}(\varphi)$ into its disjuncts.
%
%\emph{We note that symbolic execution with goals is crucial for obtaining finite proof trees in the presence of possibly unbounded  loops  and recursive calls};
%
%\item \emph{weakening} $\varphi$ to some other goal $\varphi'$: this amounts  to applying the \emph{implication} derived rule of RL.
%If $\varphi'$ is the right-hand side of a goal in $G'$ then that goal is proved, and $\varphi$ is eliminated from the set of patterns in the resulting node.
%\end{itemize}
%The procedure stops when a node with an empty set of patterns is encountered. If this happens on has constructed a proof of  $\S \cup G \vdash  \Delta_{\S}(G)$ and thus, $\S \models G$.
%
%
%\begin{example}
%We prove using the above-described method that, whenever it terminates, the  \IMP program in Figure~\ref{fig:sum} computes the sum of natural numbers up to a symbolic bound $n$.
%We use  the two following reachability-logic formulas, in which \texttt{sum} denotes the whole program and \texttt{while} denotes the while-loop: 
%\begin{eqnarray}
%&&\kall[black]{cfg}{\kall[black]{k}{\texttt{sum}} \kall[black]{env}{\texttt{n} \mapsto n, \texttt{s} \mapsto s, \texttt{i} \mapsto i}}  \pmb{\Ra} \label{eq:f1} \\
%&& \qquad \kall[black]{cfg}{\kall[black]{k}{\texttt{.}} \kall[black]{env}{\texttt{n} \mapsto n, \texttt{s} \mapsto s', \texttt{i} \mapsto i'}} \pmb{\wedge} s = n*(n+1) /2 \wedge i = n+1\nonumber \\
%&&\kall[black]{cfg}{\kall[black]{k}{\texttt{while}} \kall[black]{env}{\texttt{n} \mapsto n, \texttt{s} \mapsto s, \texttt{i} \mapsto i}} \pmb{\wedge} i \leq n+1 \wedge s = i*(i+1)/2 \pmb{\Ra} \label{eq:f2} \\
%&& \qquad \kall[black]{cfg}{\kall[black]{k}{\texttt{.}} \kall[black]{env}{\texttt{n} \mapsto n, \texttt{s} \mapsto s', \texttt{i} \mapsto i'}} \pmb{\wedge} s = n*(n+1) /2 \wedge i = n+1\nonumber
%\end{eqnarray}
%\begin{figure}[t]
%\centering{
%\begin{verbatim}
%s = 0;
%i = 0;
%while (i <=  n) {
%  s = s + i;
%  i = i + 1;
%}  
%\end{verbatim}
%}
%\caption{\label{fig:sum}\mytt{sum.imp} }
%\end{figure}
%The first formulas says that, by starting with the \texttt{sum} program and some symbolic values $n,i,s$ for \texttt{n}, \texttt{i}, and \texttt{s}, respectively
%if the program terminates with values $n',i',s'$ for the variables satisfying the expected constraint $s = n*(n+1)/2$. The second formula says that the same final pattern is reached by starting at the \texttt{while} loop with the constraint $s= i*(i+1)/2$, which acts like a loop invariant. 
%
%The  two formulas constitute the set of goals $G$ to prove. The first step consists in computing the set of goals $G' = \Delta_\S(G)$, which amounts to symbolically executing the semantics of the first instruction of each of the goals. For the first goal, the instruction \texttt{s = 0} assigns $0$ to \texttt{s} in the \textsf{env} cell;
%and in the second goal, the \texttt{while} loop is rewritten into an \texttt{if} statement according to the \IMP semantics.
%\vr{restul exemplului de scris dupa ce avem toolul.}
%
%The rest off the process consists in building a proof tree for $\S \cup G \vdash  \Delta_{\S}(G)$. We start  from an initial that contains the two patterns ${\varphi'_1, \varphi'_2}$, which are the left-hand sides of $G'$. We call $\varphi$   both their  right-hand sides (they are the same).
%\begin{itemize}
%\item We apply \emph{symbolic execution with $\S$}  to $\varphi'_1$, until the \texttt{while} loop is reached;
%\item Then we  apply \emph{symbolic execution with the goal}~(\ref{eq:f2}), and directly obtain $\varphi$;
%\item Hence, the pattern $\varphi'_1$ is eliminated from the current node; only $\varphi'_2$ is left;
%\item We apply \emph{symbolic execution with $\S$}  to $\varphi'_1$, until it is transformed into 
%\begin{itemize}
%\item  a pattern implying $\varphi$, which is thus eliminated from the current node;
% \item a pattern to which \emph{symbolic execution with the goal}~(\ref{eq:f2}) is applicable. This  generates 
% a pattern implying $\varphi$, which is removed from the  node.
%\end{itemize}
%\end{itemize}
%We have obtained a node with an empty set of patterns. This constitutes a proof of $\S \cup G \vdash  \Delta_{\S}(G)$ and therefore of the validity of  both goals in the set $G$.
%\end{example}


\section{A Prototype Implementation}
\label{sec:tool}

In this section we describe the implementation of a tool \kcheck, which uses the deductive system that we have defined in Figure~\ref{fig:altrl} in order to verify $\S \models \G$, for a given language semantics $\S$ and a set of reachability formulas (goals) $\G$. The implementation is part of the \K tools suite~\cite{k} and it has been developed on top of our symbolic execution framework~\cite{ArusoaieLR2013SLE}. \K is a rewrite-based executable semantics framework in which programming languages, type systems, and formal analysis tools can be defined. Beside some toy languages used for teaching, there are a few real-word programming languages, supporting different paradigms, that have been successfully defined in \K: Scheme~\cite{meredith-hills-rosu-2007-scheme}, Verilog~\cite{meredith-katelman-meseguer-rosu-2010-memocode}, C~\cite{ellison-rosu-2012-popl}, Python~\cite{guth-2013-thesis}, Java~\cite{java}, OCaml~\cite{ocaml}. An example of a \K definition can be found in Section~\ref{sec:example}. The framework also includes support for symbolic execution. One can execute programs having symbolic inputs using a transformed definition of a language which is generated automatically from its original \K definition~\cite{ArusoaieLR2013SLE}. The result of the symbolic execution consists in a set of logical constraints corresponding to different program paths. In terms of implementation, our prototype reuses some components of the \K framework: parsing, compilation steps,  support for symbolic execution, and the connections to the Maude's~\cite{DBLP:conf/rta/Meseguer00} model-checker and the Z3 SMT solver~\cite{DBLP:conf/tacas/MouraB08}. Since our approach is parametric in the formal definition of the language, \kcheck\ can also benefit in the future from the new language definitions. 

The tool completes two stages during its execution: it builds a new  definition and then performs verification. Given a language definition $\S$ and a set of RL formulas $\G$, \kcheck\ produces a new definition $\symb{\S} \cup \G$, where $\symb{\S}$ is defined as in Section~\ref{sec:sym}. If $\symb{\S}$ is weakly well-definable (Def.~\ref{def:wwdf}) but not weakly well-defined (Def.~\ref{def:wwd}) then we use $(\symb{\S})^\Delta$ instead of $\symb{\S}$. This new definition is used to perform symbolic execution of the patterns in left hand sides of formulas in $\Delta_\S(\G)$, in order to find a proof of $\S \cup \G \vdash \Delta_\S(\G)$ with the proof system in Fig.~\ref{fig:altrl}.

Computing all the successors of a pattern by applying rules from $\symb{\S}$ corresponds to applying the $\textsf{SymbolicStep}$ deduction rule. Computing the successor of a pattern by using a rule from $\G$ corresponds to applying $\textsf{CircularHypothesis}$. The rules from $\G$ are only applied to patterns from the left hand side of $\Delta_\S(\G)$ or to  their successors obtained by derivation. This is achieved using a labeling mechanism that singles out the patterns to which rules from $\G$ can be applied, and, moreover, this gives priority to rules in $\G$ over rules in $\symb{\S}$. $\textsf{CaseAnalysis}$ is implicitly applied by splitting disjunctive patterns $\bigvee_{i}(\pattern{\pi_i}{\phi_i})$ obtained by $\textsf{SymbolicStep}$ and $\textsf{CircularHypothesis}$ back into elementary patterns $\pattern{\pi_i}{\phi_i}$. $\textsf{Implication}$ is applied at the end of the branches of the proof tree, in order to check that the current pattern implies the right hand side of the current goal. This has to succeed in all branches for the proof to succeed.  Finally, $\textsf{Transitivity}$  is used to build proof trees in the deductive system in Fig.~\ref{fig:altrl} from symbolic execution trees.


%\dl{Cred ca Vlad are dreptate, spatiul nu ne permite sa punem in corpul articolului exemplele de mai jos, asa ca le putem pune intr-o anexa. Textul de pana acum cam spune ce face prototipul. Putem mentiona doar pe ce limbaje a fost testat si cam ce programe au fost verifcate. Trebuie sa spunem ca, fiind un prototip, performantele nu pot fi comparate deocamdata cu toolurile specializate, dar demonstreaza ca e posibil sa construim verifcatoare pornind de la sistemul de deductie generic RL.\\
%Mai mult decat atat, putem avea doua anexe: una cu demonstratiile si alta cu exemplele.}

We have used \kcheck\ to prove \texttt{gcd.imp} (Figure~\ref{fig:gcd}) as sketched in Example~\ref{ex:gcdproof}. The  tool has also been used to prove all the \IMP programs from~\cite{Apt}. In the rest of the section we  illustrate the verification of  a  parallel program in order to show that our approach is language-independent and can deal with nontrivial proofs.

%\vr{as pomeni de celalalt limbaj abia dupa ce facem exemplul din primul limbaj ca sa nu confuzam cititorul.}
%
%\subsubsection{Greatest common divisor (\texttt{gcd}).} 
%
%The ingredients needed to prove that the program shown in Figure~\ref{fig:gcd} is correct, are the \IMP semantics (Figure~\ref{impsem}) and the reachability rules (\ref{eq:specgcd}),(\ref{eq:specgcd2}), and (\ref{eq:specgcd3}). 
%
%, in the sense that it really computes the greatest common divisor. First, let us consider the following code macros {\small $\mathtt{GCD} \eqbydef$ \texttt{x=a;y=b;while(y>0) \{r=x\%y;x=y;y=r;\}}}, {\small $\mathtt{LOOP} \eqbydef$ \texttt{while(y>0)\{r=x\%y;x=y;y=r;\}}}, and {\small $\mathtt{BODY} \eqbydef$ \texttt{\{r=x\%y;x=y;y=r;\}}}. In terms of reachability logic we want to prove the following property for {\small$\mathtt{GCD}$}:
%%\vspace{-1ex}{\small
%\[
%{\pattern{{\kall[black]{k}{\mathtt{GCD}}\kall[black]{env}{\texttt{a}{\mapsto}a~\texttt{b}{\mapsto}b~\texttt{x}{\mapsto}x~Rest}}}{a \geq 0 \wedge b \geq 0}}
%\pmb{\Ra}%\vspace*{-1ex}\]\[
%{\pattern{{\kall[black]{k}{\kdot}\kall[black]{env}{\texttt{a}{\mapsto}a~\texttt{b}{\mapsto}b~\texttt{x}{\mapsto}x'~Rest'}}}{x' = gcd(a, b)}}
%%%\vspace*{-1ex}
%\]
%}
%\noindent The proof of this reachability rule cannot be done in a straightforward manner.
%\vr{Nu cred ca trebuie folosit "unfortunately". }
% The reason is that the left hand side of the rule contains a loop, and during the proving process the only possibility to prove the loop is to apply $\textsf{[CircularHypothesis]}$. Otherwise, the proof tree can be infinite. For the loop we need the following reachability rule:
%%\vspace{-1ex}{\small
%\[
%{\pattern{{\kall[black]{k}{\mathtt{LOOP}}\kall[black]{env}{\texttt{a}{\mapsto}a~\texttt{b}{\mapsto}b~\texttt{x}{\mapsto}x~\texttt{y}{\mapsto}y~Rest}}}{x \geq 0 \wedge y \geq 0 \wedge gcd(a, b) = gcd(x,y)}}
%\pmb{\Ra}%\vspace*{-1ex}\]\[
%{\pattern{{\kall[black]{k}{\kdot}\kall[black]{env}{\texttt{a}{\mapsto}a~\texttt{b}{\mapsto}b~\texttt{x}{\mapsto}x'~\texttt{y}{\mapsto}y'~Rest'}}}{x' \geq 0 \wedge y' = 0 \wedge gcd(a, b) = gcd(x',y')}},
%%%\vspace*{-1ex}
%\]
%}
%and a reachability rule to prove the body of the loop:
%%\vspace{-1ex}{\small
%\[
%{\pattern{{\kall[black]{k}{\mathtt{BODY}}\kall[black]{env}{\texttt{a}{\mapsto}a~\texttt{b}{\mapsto}b~\texttt{x}{\mapsto}x~\texttt{y}{\mapsto}y~Rest}}}{x \geq 0 \wedge y > 0 \wedge gcd(a, b) = gcd(x,y)}}
%\pmb{\Ra}%\vspace*{-1ex}\]\[
%{\pattern{{\kall[black]{k}{\kdot}\kall[black]{env}{\texttt{a}{\mapsto}a~\texttt{b}{\mapsto}b~\texttt{x}{\mapsto}x'~\texttt{y}{\mapsto}y'~Rest'}}}{x' \geq 0 \wedge y' \geq 0 \wedge gcd(a, b) = gcd(x',y')}}.
%%%\vspace{-1ex}
%\]}
%The reachability rule for {\small $\mathtt{LOOP}$} proves that after the execution of {\small $\mathtt{LOOP}$} the invariant is preserved: if the execution starts in a state where {\small $x \geq 0 \wedge y \geq 0 \wedge gcd(a, b) = gcd(x,y)$} holds then it ends up in a state where the new values of variables {\small $\mathtt{x}$} and {\small $\mathtt{y}$}, namely {\small $x'$} and {\small $y'$}, satisfy {\small $x' \geq 0 \wedge y' \geq 0 \wedge gcd(a, b) = gcd(x',y')$}. Moreover, after the execution, the negation of the loop condition {\small $\neg (y > 0)$} must also hold, which induces {\small $y' = 0$} in the postcondition. For {\small $\mathtt{BODY}$} we proceed as in the traditional approach:  we assume the invariant and the loop condition, which is {\small $x \geq 0 \wedge y > 0 \wedge gcd(a, b) = gcd(x,y)$},  and after the execution {\small $x' \geq 0 \wedge y' \geq 0 \wedge gcd(a, b) = gcd(x',y')$} must be satisfied.

%If these reachability rules are saved in a file {\small $\mathtt{gcd.rl}$} and the semantics of \IMP in {\small $\mathtt{imp.k}$} then we can call \kcheck as follows:
%%\vspace{-1ex}
%{\small
%\begin{verbatim}
%    $ kcheck imp.k -rlfile gcd.rl
%\end{verbatim}
%}
%%\vspace{-1ex}
%
%The tool generates the semantics $\S+\G$ and verifies the reachability rules from {\small $\mathtt{gcd.rl}$} one by one. The output corresponding to the (\ref{eq:specgcd2}) is shown below:\\
%
%\noindent{\small
%\texttt{Verifying (1)...}\\
%\texttt{Solution 1, State 3:}\\
%\texttt{<path-condition>\\
%   $gcd(a,b) = gcd(x, y) \land y >= 0 \land x >= 0 \land  \lnot (y <= 0) \land\\ 
%    gcd(a, b) = gcd(x, y) \land y > 0 \land x >= 0 \land\\
%    gcd(a, b) = gcd(symInt(1),symInt(2)) \land symInt(2) >= 0 \land symInt(1) >= 0 \land\\
%    gcd(a, b) = gcd(symInt(1), symInt(2)) \land symInt(2) >= 0 \land symInt(1) >= 0 \land\\ 
%    gcd (a,b ) = gcd (x', y') \land y' = 0 \land x' >= 0$\\ </path-condition>}\\
%\texttt{<k> $\kdot$ </k>\\
%<state> a $\mapsto$ $a$ b |-> $b$ r |-> $r'$ x |-> $x'$ y |-> $y'$ </state>
%}\\
%\texttt{Solution 2, State 4:}\\
%\texttt{<path-condition>\\
%    $gcd(a,b) = gcd(x, y) \land y >= 0 \land x >= 0 \land y <= 0$\\
%</path-condition>}\\
%\texttt{<k> $\kdot$ </k>\\
%<state> a $\mapsto$ $a$ b |-> $b$ r |-> $r$ x |-> $x$ y |-> $y$ </state>
%}\\\\
%}
%
%
%The reachability rules are automatically numbered starting with 0, considering the order declared in the {\small $\mathtt{gcd.rl}$} file. In our case, the first verified reachability rule is (\ref{eq:specgcd3}). An empty \texttt{<k> $\kdot$ </k>} cell shows that the proof of this rule was successful. If the proof had failed then the cell would have contained the last configuration, which is the point where the proof got stuck. In the \texttt{<state>} cell we can  observe the effect of the executed code over the values of variables, \texttt{r} and \texttt{y} being mapped to $x\%y$, while \texttt{x} is mapped to $y$. The \texttt{<path-condition>} cell contains the formula collected during the symbolic execution of \texttt{body}. The constraints over $x$ and $y$ are collected from the initial condition given in the reachability rule $gcd(a, b) = gcd(x, y) \land y > 0 \land x >= 0$ and from the $\%$ operation condition, which is $\lnot(y = 0)$. For other rules, the path condition may include also formulas induced by circularities. The second output, which is the proof of (\ref{eq:specgcd2}), has two solutions corresponding to the cases when the loop condition holds or not. If the condition holds, then the rule (\ref{eq:specgcd3}) can be applied as circularity, thus adding its constraints to the current path condition. We can also observe that the path condition contains some symbolic values $symInt(1)$ and $symInt(2)$. Those are generated by the tool for variables which appear only in the right hand side of a reachability rule, when the circularity is applied. This helps users to write the reachability rules in a more uniform and elegant way. At the second iteration of the loop, (\ref{eq:specgcd2}) is applied as circularity, and thus it adds its own conditions to the path condition.
%The last proof corresponds to  (\ref{eq:specgcd}) and uses (\ref{eq:specgcd2}) as circularity. Since none of the proofs have failed then (\ref{eq:specgcd}) is proved successfully, so \texttt{gcd} is correct w.r.t. (\ref{eq:specgcd}).
%
%\vr{eu as alege unul din goaluri l-as trata mai in detaliu, si le-as explica mai rapid  pe celelalte ... altfel nu se intelege, sunt prea multe detalii dupa parerea mea.}
%\aa{pe care?}
%
%There are cases when the formulas we want to prove may contain different functions (e.g. {\small $gcd$}) for which we don not have a proper translation for the SMT solver. If so, the tool sends them by default to the SMT solver as uninterpreted functions. However, \kcheck allows users to add their own definitions for functions, which may simplify the formula before sending it to the solver. 

%\vspace{-2ex}
\subsection{Verifying a parallel program:{ $\mathtt{FIND}$}} The  program is borrowed from~\cite{Apt}. Given an integer array $a$ and a constant $N \geq 1$, the  program in Figure~\ref{fig:find}  finds the smallest index $k \in \{1, \ldots, N\}$ such that $a[k] > 0$. If such an index $k$ does not exists then $N+1$ is returned. It is a  \emph{disjoint} parallel program, which means that its parallel components  only have reading access to the  variable $a$ they share.

\begin{figure}[t]

\centering
\begin{tabular}{ l  c }
\begin{minipage}{.33\textwidth}
\begin{verbatim}
i = 1; 
j = 2;
oddtop = N + 1; 
eventop = N + 1;
S1 || S2;
if (oddtop > eventop) 
  then { k = eventop; }
  else { k = oddtop; }
\end{verbatim} 
\end{minipage}
&
\begin{minipage}{.5\textwidth}
\begin{verbatim}
S1 = while (i < oddtop) {
       if (a[i] > 0) then { oddtop = i; }
       else { i = i + 2; }
     }
S2 = while (j < eventop) {
       if (a[j] > 0) then { eventop = j; }
       else { j = j + 2; }
     }
\end{verbatim}
\end{minipage}
\end{tabular}
\caption{\label{fig:find} $\mathtt{FIND}$ program.}
%\vspace{-5ex}
\end{figure}

In order to verify {\small $\mathtt{FIND}$}, we have defined in \K the semantics of a parallel language which provides assignments, if-statements, loops, arrays, dynamic threads, and the \verb^||^ operator, which executes in parallel two threads corresponding to \verb^S1^ and \verb^S2^. To facilitate the semantics of threads, more specifically to naturally give them access to their parent's variables, we split  the program state into an environment $\kall[black]{env}{}$ and a store $\kall[black]{st}{}$.  An environment maps variable names into locations, while a store maps locations into values. Each thread $\kall[black]{th}{}$ has its own computations $\kall[black]{k}{}$ and environment $\kall[black]{env}{}$ cells, while $\kall[black]{st}{}$ is shared among the threads. Threads also have an $\kall[black]{id}{}$  (identifier) cell. The   configuration is shown below.
The $^+$ on the $\kall[black]{th}{}$  cell says that the cell contains at least one thread:%in Figure~\ref{fig:pcfg}. 
%\begin{figure}
%\vspace{-2.7ex}
$$\kall[black]{cfg}{
\kall[black]{th^+}{
\kall[black]{k}{\mathit{Code}}
\kall[black]{env}{\mathit{Map}_{\mathit{Id,Int}}}
\kall[black]{id}{\mathit{Int}}
}
\kall[black]{st}{\mathit{Map}_{\mathit{Int,Int}}}
}$$

%\vspace{-1.3ex}

%\caption{\label{fig:pcfg} 
%Configuration for the (parallel) language. 
%The $^+$ near $\kall[black]{th}{}$ cell represents the multiplicity (one or more) of the cell.
%}
%\end{figure}xx
Most of the syntactical constructs of this language have almost the same semantics as in \IMP (e.g. assignments, if-statements, loops). However, the language is more complex than \IMP, since it supports arrays and threads. The main thread, identified by 0, creates a new $\kall[black]{th}{}$ cell, each time when the operator \verb^||^ is met. For instance, when \verb^S1||S2;^ has to be executed, the main thread creates $\kall[black]{th}{\kall[black]{k}{\mathit{S1}}\kall[black]{env}{\rho}\kall[black]{id}{id_1}}$ and $\kall[black]{th}{\kall[black]{k}{\mathit{S2}}\kall[black]{env}{\rho}\kall[black]{id}{id_2}}$, where $\rho$ is the map of variables inherited from the main thread, and $id_1$ and $id_2$ are two fresh identifiers. Thread 0 waits for these two threads to finish %the execution of  \verb^S1^ and \verb^S2^, 
and then computes the return value $k$. 

The \verb^||^ operator yields a non-deterministic behavior of {\small $\mathtt{FIND}$}.
%The main concern is that {\small $\mathtt{FIND}$} can generate more than one computation starting in a given initial state. 
However, in ~\cite{Apt} the authors prove that all computations of a disjoint parallel program starting in the same initial state produce the same output.
% So, all the computations of a disjoint parallel program are equivalent to the sequential execution of its components.
 For program verification this observation  simplifies matters because 
it allows independent verification of the parallel code, without considering the  interleavings caused by parallelism.


\begin{figure}
\small
\begin{tabular}{|l|}
\hline
\verb^CODE MACROS^ \\
\hline
\begin{minipage}{\textwidth}
\begin{tabular}{lcl}
\verb^INIT^ & $\eqbydef$ & \verb^i = 1; j = 2; oddtop = N + 1; eventop = N + 1;^\\
\verb^BODY1^ & $\eqbydef$ & \verb^{if (a[i] > 0) then { oddtop = i; } else { i = i + 2; }}^\\
\verb^BODY2^ & $\eqbydef$ & \verb^{if (a[j] > 0) then { eventop = j; } else { j = j + 2; }}^\\
\verb^S1^ & $\eqbydef$ & \verb^while (i < oddtop) BODY1^\\
\verb^S2^ & $\eqbydef$ & \verb^while (j < eventop) BODY2^\\
\verb^MIN^ & $\eqbydef$ & \verb^if (oddtop > eventop) then { k = eventop; } else { k = oddtop; }^\\
\verb^FIND^ & $\eqbydef$ & \verb^INIT S1||S2; MIN^\\
\end{tabular}
\end{minipage}~\\
\hline
\hline
\textit{Formula macros}\\
\hline
\begin{minipage}{\textwidth}
\small
\begin{tabular}{lcl}
$pre$ & $\eqbydef$ & $N \geq 1$\\
$p_1$ & $\eqbydef$ & $1 \leq o \leq N + 1 \land i \% 2 = 1 \land 1 \leq i \leq o + 1$ \\
             & & $\land ({\forall}_{1 \leq l < i})(l \% 2 = 1 \implies a[l] \leq 0) \land (o \leq N \implies a[o] > 0)$\\
$p_1'$ & $\eqbydef$ & $1 \leq o' \leq N + 1 \land i' \% 2 = 1 \land 1 \leq i' \leq o' + 1$ \\
             & & $\land ({\forall}_{1 \leq l < i'})(l \% 2 = 1 \implies a[l] \leq 0) \land (o' \leq N \implies a[o'] > 0)$\\
$q_1$ & $\eqbydef$ & $1 \leq o' \leq N + 1 \land ({\forall}_{1 \leq l < o'})(l \% 2 = 1 \implies a[l] \leq 0) \land (o' \leq N \implies a[o'] > 0)$\\ 
$p_2$ & $\eqbydef$ & $2 \leq e \leq N + 1 \land j \% 2 = 0 \land 2 \leq j \leq e + 1$ \\
             & & $\land ({\forall}_{1 \leq l < j})(l \% 2 = 0 \implies a[l] \leq 0) \land (e \leq N \implies a[e] > 0)$\\
$p_2'$ & $\eqbydef$ & $2 \leq e' \leq N + 1 \land j' \% 2 = 0 \land 2 \leq j' \leq e' + 1$ \\
             & & $\land ({\forall}_{1 \leq l < j'})(l \% 2 = 0 \implies a[l] \leq 0) \land (e' \leq N \implies a[e'] > 0)$\\
$q_2$ & $\eqbydef$ & $2 \leq e' \leq N + 1 \land ({\forall}_{1 \leq l < e'})(l \% 2 = 0 \implies a[l] \leq 0) \land (e' \leq N \implies a[e'] > 0)$\\ 
$m$ & $\eqbydef$ & $1 \leq min(o,e) \leq N + 1 \land ({\forall}_{1 \leq l < min(o,e)})(a[l] \leq 0) $\\
                 &&$\land (min(o,e) \leq N \implies a[min(o,e)] > 0)$\\
%$m'$ & $\eqbydef$ & $1 \leq min(o',e') \leq N + 1 \land ({\forall}_{1 \leq l < min(o',e')})(a[l] \leq 0) $\\
%                 &&$\land (min(o',e') \leq N \implies a[min(o',e')] > 0)$\\
$post$ & $\eqbydef$ & $1 \leq k' \leq N + 1 \land ({\forall}_{1 \leq l < k'})(a[l] \leq 0) \land (k' \leq N \implies a[k'] > 0)$
\end{tabular}
\end{minipage}
\\
\hline
\hline
{\it Map macros for environment and store}\\
\hline
\begin{minipage}{\textwidth}
\begin{tabular}{lcl}
$Env$ & $\eqbydef$ & $\mathtt{a}\mapsto {\bf a}~\mathtt{i}\mapsto {\bf i} ~\mathtt{j}\mapsto {\bf j}~\mathtt{oddtop}\mapsto {\bf o}~\mathtt{eventop}\mapsto {\bf e}~\mathtt{N}\mapsto {\bf N}~\mathtt{k}\mapsto {\bf k}$\\
$St$ & $\eqbydef$ & ${\bf a} \mapsto a~{\bf i} \mapsto i ~{\bf j} \mapsto j ~{\bf o} \mapsto o ~{\bf e} \mapsto e ~{\bf N} \mapsto N~{\bf k} \mapsto k$\\
$St'$ & $\eqbydef$ & ${\bf a} \mapsto a~{\bf i} \mapsto i' ~{\bf j} \mapsto j' ~{\bf o} \mapsto o' ~{\bf e} \mapsto e' ~{\bf N} \mapsto N~{\bf k} \mapsto k'$\\
\end{tabular}
\end{minipage}\\
\hline
\hline
Reachability rules\\
\hline
\begin{minipage}{\textwidth}
\begin{tabular}{lcl}
%\setcounter{equation}{1}
%\numberwithin{equation}{section}
$(1)$~$\kall[black]{th}{\kall[black]{k}{\mathtt{INIT}}\kall[black]{env}{Env}}\kall[black]{st}{St} \land pre$
&
$\Ra$
&
$\kall[black]{th}{\kall[black]{k}{\kdot}\kall[black]{env}{Env}}\kall[black]{st}{St'}\land (p_1' \land p_2')$\\

$(2)$~$\kall[black]{th}{\kall[black]{k}{\mathtt{BODY1}}\kall[black]{env}{Env}}\kall[black]{st}{St} \land i < o \land p_1$
&
$\Ra$
&
$\kall[black]{th}{\kall[black]{k}{\kdot}\kall[black]{env}{Env}}\kall[black]{st}{St'}\land p_1'$\\

$(3)$~$\kall[black]{th}{\kall[black]{k}{\mathtt{S1}}\kall[black]{env}{Env}}\kall[black]{st}{St} \land i < o \land p_1$
&
$\Ra$
&
$\kall[black]{th}{\kall[black]{k}{\kdot}\kall[black]{env}{Env}}\kall[black]{st}{St'}\land o' \leq i' \land p_1' \land q_1$\\

$(4)$~$\kall[black]{th}{\kall[black]{k}{\mathtt{BODY2}}\kall[black]{env}{Env}}\kall[black]{st}{St} \land j < e \land p_2$
&
$\Ra$
&
$\kall[black]{th}{\kall[black]{k}{\kdot}\kall[black]{env}{Env}}\kall[black]{st}{St'}\land p_2'$\\

$(5)$~$\kall[black]{th}{\kall[black]{k}{\mathtt{S2}}\kall[black]{env}{Env}}\kall[black]{st}{St} \land j < e \land p_2$
&
$\Ra$
&
$\kall[black]{th}{\kall[black]{k}{\kdot}\kall[black]{env}{Env}}\kall[black]{st}{St'}\land e' \leq j' \land p_2' \land q_2$\\

$(6)$~$\kall[black]{th}{\kall[black]{k}{\mathtt{S1||S2;}}\kall[black]{env}{Env}}\kall[black]{st}{St} \land p_1 \land p_2$
&
$\Ra$
&
$\kall[black]{th}{\kall[black]{k}{\kdot}\kall[black]{env}{Env}}\kall[black]{st}{St'}\land q_1 \land q_2$\\

$(7)$~$\kall[black]{th}{\kall[black]{k}{\mathtt{MIN}}\kall[black]{env}{Env}}\kall[black]{st}{St} \land q_1 \land q_2 \land m$
&
$\Ra$
&
$\kall[black]{th}{\kall[black]{k}{\kdot}\kall[black]{env}{Env}}\kall[black]{st}{St'}\land post$\\

$(8)$~$\kall[black]{th}{\kall[black]{k}{\mathtt{FIND}}\kall[black]{env}{Env}}\kall[black]{st}{St} \land pre$
&
$\Ra$
&
$\kall[black]{th}{\kall[black]{k}{\kdot}\kall[black]{env}{Env}}\kall[black]{st}{St'}\land post$\\

\end{tabular}
\end{minipage}\\
\hline
\hline
Corresponding proofs given by \kcheck\\
\hline
\begin{minipage}{\textwidth}
\begin{tabular}{l}
$(1)$~$\textsf{[SymbolicStep]},\textsf{[SymbolicStep]}, \textsf{[SymbolicStep]}, \textsf{[SymbolicStep]},\textsf{[Implication]}$\\
$(2)$~$\textsf{[CaseAnalysis]},(\textsf{[SymbolicStep]},\textsf{[Implication]})\lor(\textsf{[SymbolicStep]},\textsf{[Implication]})$\\
$(3)$~$\textsf{[SymbolicStep]}, \textsf{[CaseAnalysis]}, (\textsf{[Implication]} \lor $(2)$,$(3)$,\textsf{[Implication]})$\\
$(4)$~$\textsf{[CaseAnalysis]},(\textsf{[SymbolicStep]},\textsf{[Implication]})\lor(\textsf{[SymbolicStep]},\textsf{[Implication]})$\\
$(5)$~$\textsf{[SymbolicStep]}, \textsf{[CaseAnalysis]}, (\textsf{[Implication]} \lor $(4)$,$(5)$,\textsf{[Implication]})$\\
$(6)$~$\textsf{[SymbolicStep]}, $(3)$,$(5)$, \textsf{[Implication]}$\\
$(7)$~$\textsf{[CaseAnalysis]},(\textsf{[SymbolicStep]},\textsf{[Implication]})\lor(\textsf{[SymbolicStep]},\textsf{[Implication]})$\\
$(8)$~$$(1)$, $(6)$, $(7)$, \textsf{[Implication]}$\\
\end{tabular}
\end{minipage}\\\hline
\end{tabular}
\caption{\small \label{fig:findrl} RL formulas necessary to verify {\small $\mathtt{FIND}$}. We use $\mathtt{a}$, $\mathtt{i}$, $\mathtt{j}$, $\mathtt{oddtop}$, $\mathtt{eventop}$, $\mathtt{N}$, $\mathtt{k}$ to denote program variables, {\bf a}, {\bf i}, {\bf j}, {\bf o}, {\bf e}, {\bf N}, {\bf k} to denote locations, and $a$, $i$, $j$, $o$, $e$, $N$, $k$ for variables values. 
%We also use $i'$, $j'$, $o'$, $e'$, $k'$ to refer the new values of $i$, $j$, $o$, $e$, $k$. 
By $min(o,e)$ we refer the mathematical function that returns the minimum of $o$ and $e$.  \textsf{CaseAnalysis}  splits the proof in two goals separated by $\lor$, while the application of \textsf{CircularHypothesis} where $\alpha$ is the $i$-the formula is represented as $(i)$.
}
\end{figure}


Figure~\ref{fig:findrl} shows all the ingredients that we used to prove {\small $\mathtt{FIND}$} using our tool. At the figure's top we show the code macros that we use in our reachability formulas. Below the code macros we include the formulas  corresponding to the pre/post conditions and invariants used by the authors of~\cite{Apt} in their proof. Next, we show the reachability formulas that were  constructed from the above pre/post conditions and invariants. Finally we show the proofs  given by \kcheck. 
%Note that {\small $\mathtt{FIND}$} is proved following the same strategy as in ~\cite{Apt}, where the authors prove incrementally properties for different pieces of code, and then the entire program. 

The proof tree corresponding to sequential of code (e.g. {\small $\mathtt{INIT}$}) has  a single branch, while the proof tree corresponding to code containing loops or if-statements can have multiple branches. Some examples are the proofs for the reachability rules $(3)$, $(5)$, and $(7)$, where  \textsf{CaseAnalysis} splits the proof in two branches. The proof tree for the reachability formula $(8)$, corresponding to the specification of {\small $\mathtt{FIND}$},  has a single branch because it uses circularities, which do not split the proof tree, making the proof tree more compact.

The verification of {\small $\mathtt{FIND}$} might look difficult, but this is because its verification is hard in general, no matter what underlying logic one uses. Our proof has  the same structures as the proof from~\cite{Apt}, except  for the fact that we express program properties as reachability formulas. However, when performing mechanised verification, the pre/post conditions and the invariants must be very accurate. Otherwise, the proof will fail even if, intuitively, all the formulas seem to hols. 

When using \kcheck\ to verify {\small $\mathtt{FIND}$}, we discovered  that the precondition $pre$ must be  $N\geq1$ rather than $\true$ as stated in the (non-mechanised) proof of~\cite{Apt}, and in $p_2$ the value of $j$ must be $\geq2$, a constraint also forgotten in~\cite{Apt}. 

%Moreover, \kcheck\ can also prove {\small $\mathtt{FIND}$} without proving the reachability formula associated to {\small $\mathtt{INIT}$}. This is because the tool successfully checks the precondition $p_1 \land p_2$ (which should hold before executing {\small $\mathtt{S1||S2}$}) using only the path condition given by the symbolic execution of  {\small $\mathtt{INIT}$}. 

%It takes \kcheck\  30 seconds to verify all the reachability formulas shown in Figure~\ref{fig:findrl}.  
%\dl{Trebuie mentionat ca asta include transformarea definitiei initiale si compilarea definitiei combinate.}
%\vr{Daca includem asta executia dureaza mai mult, parca Andrei spunea de 1 minut}
%\aa{E discutabil: practic toata recompilarea se face la fiecare apel de check, doar ca dureaza mult mai putin. Eu as zice sa masor exact timpul de proving si sa-l punem pe acela. Oricum, eu stiu ca tot in jur de 30 de secunde dureaza. :-)}
The formulas are nontrivial, and it took us several iterations to come up with the exact ones, during which we used the tool in a trial-and-error process. The  automatic nature of the tool, as well as the feedback it returned when it failed, were particularly  helpful during this  process. In particular symbolic execution can be used for initial debugging of programs before they are verified. 

%Considering the complexity of the proofs and the fact that the user can adjust the formulas and check immediately if they hold or not, we can conclude that our prototype implementation demonstrates that it is feasible to use our deductive system (Figure~\ref{fig:altrl}) for proving program properties. 
%. 


%\aa{Am schitat demonstratiile in Figura~\ref{fig:findrl}... nu stiu ce sa mai zic aici...}
%\vr{Cred ca mai trebuie spus cate ceva despre figura, continutul ei este bun dar trebuie descris: dam mai intai niste macrouri (nume) pentru programe si formule, apoi dam regulile de reachability care folosesc aceste macrouri, si in fine demonstratiile regulilor  sub forma de  arbori de demonstratie al sistemului din Fig.~\ref{fig:altrl}. Apoi luam un exemplu de arbore si-l explicam.}

%\vspace*{-1.5ex}

\section{Related work}
\label{sec:related}

%\vspace*{-1.5ex}
There are several tools that perform program verification using symbolic execution. Some of them are more oriented towards finding bugs~\cite{Cadar:2008:KUA:1855741.1855756}, while others are more oriented towards verification~\cite{Coen-Porisini:2001:USE:503271.503230,Jaffar:2012:TSE:2362216.2362291,Ramos:2011:PLE:2032305.2032360}. Several techniques are implemented to improve the performance of these tools, such as {\it bounded verification}~\cite{Clarke:2003:HVU:1119772.1119831} and {\it pruning} the execution tree by eliminating redundant paths~\cite{Cui:2013:VSR:2499368.2451152}. The major advantage of these tools is that they perform very well, being able to verify substantial pieces of C or assembly code, which are parts of important critical systems. On the other hand, these verifiers hardcode the logic they use for reasoning, and   verify only specific programs (e.g. written using subsets of C) for specific properties such as:  allocated memory is eventually  freed, opened files are eventually closed, file reading and writing is allowed only  on opened files, etc. 

Other approaches offer support for verification of code contracts over programs. Spec\#~\cite{Barnett:2004:SPS:2131546.2131549} is a tool developed at Microsoft  that extends C\# with constructs for non-null types, preconditions, postconditions, and object invariants. Spec\# comes with a sound programming methodology that permits specification and reasoning about object invariants even in the presence of callbacks and multi-threading. A similar approach, which provides functionality for checking the correctness of a JAVA implementation with respect to a given UML/OCL specification, is the KeY~\cite{KeY2005} tool. In particular, KeY allows to prove that after running a method, its postcondition and the class invariant holds, using Dynamic Logic~\cite{Harel84dynamiclogic} and symbolic execution. The VeriFast tool~\cite{Jacobs:2010:QTV:1947873.1947902} supports verification of single and multi-threaded C and Java programs annotated with preconditions and postconditions written in Separation Logic~\cite{Reynolds:2002:SLL:645683.664578}  All these tools are designed to verify programs that belong to a specific programming language. 

An approach closely related to ours is implemented in the MatchC tool~\cite{rosu-stefanescu-2012-oopsla}, which has beed used for verifying  several challenging  C programs such as the Schorr-Waite garbage collector.  MatchC also uses the  formalism of reachability logic for program specifications; it is, however, dedicated to a specific language.

Our approach addresses the verification problem from a different angle. We focus on \emph{language-independence}: given a
formal definition of a programming language whose semantics is defined by rewriting, we automatically generate the semantics for performing symbolic execution on that language, and build on this symbolic semantics for performing program verification.  The soundness of our approach has been proved. It relies on a Circularity Principle adapted to reachability logic, which has beed formulated in a different setting in~\cite{rosu-lucanu-2009-calco}. 

Regarding performance, our generic tool is (understandably) not
in the same league as tools targetting specific languages and/or specific program properties. We believe, however, that the building of fast language-specific verification tools can benefit from the general principles presented here, in particular, regarding the building of program-verification tools on top of symbolic execution engines.


\section{Conclusion and Future Work}
\label{sec:conclusions}

%\vspace{-1.5ex}

We have presented a    language-independent framework and tool, based on symbolic execution, for  automatically  proving  properties of programs expressed in Reachability Logic. With respect to the standard proof system of Reachability Logic our approach can be seen as
a systematic strategy for constructing proofs. The approach is proved sound and the tool implementing it is illustrated on an imperative-program example as well as on a more complex
parallel program. 

%\vspace{-2ex}

\paragraph*{Future Work.} 
Reachability Logic, as a  language-independent specification formalism, can be quite verbose and may not be easy to grasp by users who are more familiar to annotations \emph{\`a la} Hoare logic (pre/post-conditions and invariants).
Annotations are by definition language-specific since the statements that are annotated are specific to languages. However, common
statements found in many languages (conditionals, loops, functions/procedures) can share the same annotations, from which RL formulas can be automatically generated. We are planning to explore this direction in order to improve the usability of our tool,
and then use the  tool on the "real" language definitions in the \K framework~\cite{java,ocaml}.


Another future research direction is embedding our verifier in a proof assistant such as Coq~\cite{coq} in order to allow a degree of user
guidance in proofs. We envisage to encode the proof system in Figure~\ref{fig:altrl} in Coq and to use our tool \kcheck\ as an
external proof constructor. Coq requires from external tools a proof term, which in re-checks in order to accept the proof;  thus,
\kcheck\ must be enhanced to build proof terms in the Coq formalism from the proof trees it generates.

We are also planning to combine program verification with the program equivalence framework we developed in~\cite{DBLP:conf/ifm/LucanuR13}. The idea is to perform verification on an abstract  program, and, via property-preserving equivalences, to ensure that the properties also hold on more concrete versions of the verified program.

%\vspace{-3.5ex}
%\bibliographystyle{abbrv}
%\bibliography{paper}  
\newpage

\section*{Appendix A: Proofs}

\noindent \textbf{Lemma~\ref{lem:dedsymbex}.}
For each transition $\varphi \ltran{\symb{\alpha}}{}{}   \varphi'$ in the symbolic transition system, with $\varphi \eqbydef \pattern{\pi}{\phi}$ and $\alpha \eqbydef \rrule{\pattern{\pi_l}{{\phi_l}} }{\pattern{\pi_r}{\phi_r}} \in \S$, there exists a substitution $\sigma$ such that $\varphi=\pattern{\sigma(\pi_l)}{\phi}$ and  $\varphi' = \pattern{\sigma(\pi_r)}{(\phi \wedge \sigma(\phi_l) \wedge \sigma(\phi_r))}$.


\begin{proof}
Since $\alpha \eqbydef \rrule{\pattern{\pi_l}{{\phi_l}} }{\pattern{\pi_r}{\phi_r}}$, the corresponding symbolic rule $\symb{\alpha}$
is of the form~(\ref{eq:transform}), i.e, $\symb{\alpha} = (\rrule{\pattern{\pi_l} {\psi}}{\pattern{\pi_r}{(\psi \wedge \phi_l \wedge \phi_r)}})$ where $\psi$
is a fresh Boolean variable. The transition  $\varphi \ltran{\symb{\alpha}}{}{}   \varphi'$ is obtained by rewriting $\varphi \eqbydef \pattern{\pi}{\phi}$
with $\symb{\alpha}$, hence, there is a substitution $\sigma \cup {(\psi \to \phi)}$ such that $(\sigma \cup (\psi \to \phi)) (\pattern{\pi_l}{\psi}) = \pattern{\pi}{\phi}$
and  $\varphi' = (\sigma \cup (\psi \to \phi))(\pattern{\pi_r}{(\psi \wedge \phi_l \wedge \phi_r)})$. The conclusion of the lemma is obtained by applying the substitution 
$\sigma \cup (\psi \to \phi)$ in the last two  identities. \hfill $\Box$
\end{proof}

\medskip

\noindent \textbf{Lemma~\ref{obs:totalcov}.}
If $\S$ is total and $\varphi$ is derivable for $\S$ then $\S$ is a cover for~$\varphi$.  



\begin{proof}
Since $\varphi \eqbydef \pattern{\pi}{\phi}$ is derivable for $\S$, the derivative  $\Delta_\S(\varphi)$ is a nonempty disjunction, hence, the set
of rules $\S_{\pi} \subseteq \S$ that match $\pi$ is nonempty. Consider then any rule
 $\alpha_0 \eqbydef(
 \rrule{\pattern{\pi_{\alpha_0}} {\phi_{\alpha_0}}}{\varphi_{\alpha_0}}) \in \S_\pi$.
Since $\S$ is total, the disjunction $\bigvee_{(\rrule{\pattern{\pi_{\alpha_0}} {\phi'}}{\varphi'})\in \S}\phi'$ is valid, hence, so is $\bigvee_{(\rrule{\pattern{\pi_{\alpha_0}} {\phi'}}{\varphi'})\in \S}\sigma^\pi_{\pi_{\alpha_0}}(\phi')$. Since the latter disjunction is a subformula of the larger disjunction
 $ \bigvee_{\alpha \eqbydef(\rrule{\pattern{\pi_\alpha}{\phi_\alpha}} {\varphi_\alpha}) \in \S} \sigma^\pi_{\pi_\alpha}(\phi_\alpha)$, 
 we  have $\models  \bigvee_{\alpha \eqbydef(\rrule{\pattern{\pi_\alpha} {\phi_\alpha}}{\varphi_\alpha}) \in \S} \sigma^\pi_{\pi_\alpha}(\phi_\alpha)$, hence,  $\models \phi \to  \bigvee_{\alpha \eqbydef(\rrule{\pattern{\pi_\alpha}{\phi_\alpha}} {\varphi_\alpha}) \in \S} \sigma^\pi_{\pi_\alpha}(\phi_\alpha)$. 

Hence, using Definition~\ref{def:cover}, $\S$ is a cover for $\varphi$, which proves the lemma. 
\end{proof}
\medskip


\noindent \textbf{Theorem~\ref{lem:deriv}.}
If $\S'\subseteq \S$  is a cover for $\varphi$, then $\S \vdash_G \varphi \pmb{\Rightarrow} \Delta_{\S'}(\varphi)$ for any set $G$.


\begin{proof}
Let $\varphi \eqbydef \pi \land \phi$. By
Definition~\ref{def:deriv}, $\Delta_{\S'}(\varphi) \eqbydef \bigvee_{\alpha \in \S', \varphi \ltran{\symb{\alpha}}{}{}   \varphi'} \varphi'$.
 Since $\S'$ is a cover for $\varphi$ (Definition~\ref{def:cover}), $\Delta_{\S'}(\varphi)$ is
a nonempty disjunction.
Using Lemma~\ref{lem:dedsymbex} we obtain that each $\varphi' $ is of the form $\varphi' = \pattern{\sigma(\pi_r)}{(\phi \wedge \sigma(\phi_l) \wedge \sigma(\phi_r))}$, for some rule  $\alpha \eqbydef (\rrule{\pattern{\pi_l}{\phi_l}}{\pattern{\pi_r}{\phi_r}} )\in \S'$ and substitution $\sigma$ such that $\sigma(\pi_l) = \pi$. We use the notation $\sigma^{\pi_l}_{\pi}$ for this substitution  and note that it is unique (cf. Remark~\ref{rem:substunique}).

Using the above characterisation for the end-patterns $\varphi'$  of symbolic transitions and the definition of derivatives:
\begin{equation} 
\label{eq:deltas}
\Delta_{\S'}(\varphi) \equiv \bigvee_{ (\rrule{\pattern{\pi_l}{\phi_l}}{\pattern{\pi_r}{\phi_r}} )\in \S'} 
\pattern{\sigma^{\pi_l}_\pi(\pi_r)}{(\phi \wedge \sigma^{\pi_l}_\pi(\phi_l) \wedge \sigma^{\pi_l}_\pi(\phi_r))}
\end{equation}
On the other hand,  by using the derived rules  of the RL  proof system: \emph{Substitution} with the rule  $\rrule{\pattern{\pi_l}{\phi_l}}{\pattern{\pi_r}{\phi_r}}$ and substitution 
$\sigma^{\pi_l}_\pi$, and  \emph{LogicalFraming} with the FOL formula $\phi$,  we get
$\S \vdash_G \sigma^{\pi_l}_\pi (\pattern{\pi_l}{\phi_l}) \wedge \phi\pmb{\Ra} \sigma^{\pi_l}_\pi(\pattern{\pi_r}{\phi_r}) \wedge \phi$, and, using  the fact that 
 $\sigma^{\pi_l}_\pi(\pi_l) = \pi$ together with the  \textsf{Consequence} rule of RL, and remembering that FOL patternless formulas distribute over patterns, we obtain

$$\S \vdash_G \pattern{\pi}{ (\phi \wedge \sigma^{\pi_l}_\pi(\phi_l))} \pmb{\Ra} \sigma^{\pi_l}_\pi(\pattern{\pi_r)}{(\phi \wedge \sigma^{\pi_l}_\pi(\phi_r)})$$

\noindent for every semantical rule $\rrule{\pattern{\pi_l}{\phi_l}}{\pattern{\pi_r}{\phi_r}} \in \S'$.
Next, using  \emph{LogicalFraming} with the above derivation and with
  $ \sigma^{\pi_l}_\pi(\phi_l)$
and then  \textsf{Consequence}, 
 we obtain
  $$\S \vdash_G   \pattern{\pi}{ (\phi \wedge \sigma^{\pi_l}_\pi(\phi_l))}  \pmb{\Ra}  \sigma^{\pi_l}_\pi(\pattern{\pi_r)}{(\phi \wedge \sigma^{\pi_l}_\pi(\phi_l) \wedge  \sigma^{\pi_l}_\pi(\phi_r))}$$ 
  for every  rule 
  $\rrule{\pattern{\pi_l}{\phi_l}}{\pattern{\pi_r}{\phi_r}} \in \S'$.
  Using  \textsf{CaseAnalysis} and  \textsf{Consequence}:
  
$$\S \vdash_G \rrule{\pattern{\pi}{(\phi \wedge \hspace{-4ex} \bigvee_{{{\pi_l}\pmb{\wedge}{\phi_l}}\pmb{\Ra}{{\pi_r}\pmb{\wedge}{\phi_r}{}} \in \S'}   \hspace{-4ex}\sigma^{\pi_l}_\pi(\phi_l))}~~~}
{ \hspace{-3ex}\bigvee_{\rrule{\pattern{\pi_l}{\phi_l}}{\pattern{\pi_r}{\phi_r}} \in \S'}  \hspace{-4ex} \pattern{\sigma^{\pi_l}_\pi(\pi_r)}{(\phi \wedge \sigma^{\pi_l}_\pi(\phi_l) \wedge  \sigma^{\pi_l}_\pi(\phi_r))}}
$$

We know from (\ref{eq:deltas}) that  the right-hand side of the above is $\Delta_{\S'}(\varphi)$. To prove $\S \vdash_G \varphi \Rightarrow \Delta_{\S'}(\varphi)$ there only  remains to prove  $(\diamondsuit)$: the condition in the left-hand side:
$(\phi \wedge \bigvee_{\rrule{\pattern{\pi_l}{\phi_l}}{\pattern{\pi_r}{\phi_r}} \in \S'}  \sigma^{\pi_l}_\pi(\phi_l))$
is logically equivalent to $\phi$ in FOL. 

Finally, since  $\S'$ is a cover for $\varphi$, we obtain, using Definition~\ref{def:cover}, the validity  of $ \phi \to \bigvee_{\rrule{\pattern{\pi_l}{\phi_l}}{\pattern{\pi_r}{\phi_r}} \in \S'}  \sigma^{\pi_l}_\pi(\phi_l)$,
which proves $(\diamondsuit)$ and the lemma. 
\end{proof}


\medskip


\noindent \textbf{Lemma~\ref{lem:sdeltaequivs}.}
$\S \models \varphi \pmb{\Ra} \varphi'$ iff $\S^\Delta \models \varphi \pmb{\Ra} \varphi'$.


\begin{proof}
$(\Rightarrow)$ From $\S \models \varphi \pmb{\Ra} \varphi'$ we obtain that for each terminating configuration $\gamma \in \T$ and valuation $\rho$
such that $(\gamma,\rho) \models \varphi$, there is $\gamma' \in \T$ and a path $\gamma \ltran{\alpha^*}{}{\S} \gamma'$, with $\alpha^* \in \S^*$,  such that $(\gamma',\rho)  \models \varphi'$. We prove by induction on the length of the sequence $\alpha^*$ that $(\spadesuit)$: $\gamma \ltran{\alpha^*}{}{\S} \gamma'$, which implies  the direct $(\Rightarrow)$ implication.

The base case of $(\spadesuit)$ is trivial. For the inductive step, we use the fact that each transition $\gamma_1  \ltran{\alpha}{}{\S} \gamma_2$
is induced by semantical rule $\alpha \eqbydef \rrule{\pattern{\pi}{\phi}}{\varphi}\in \S$ with a valuation $\rho$. Then, the corresponding rule $\rrule{\pi}{\Delta_\S(\pi)} \in \S^\Delta$ induces a corresponding  transition $\gamma_1  \ltran{\alpha}{}{\S^\Delta} \gamma_2$ with the same valuation $\rho$.

$(\Leftarrow)$ By analogy with the direct implication. The only difference  is in the inductive step:  each transition $\gamma_1  \ltran{\alpha}{}{\S^\Delta} \gamma_2$
is induced by semantical rule $\alpha^{\Delta} \eqbydef \rrule{\pi}{\Delta_\S(\pi)}{} \in \S^\Delta$ with a valuation $\rho$. Then, the rule $ \alpha \eqbydef \rrule{\pattern{\pi}{\phi}}{\varphi}\in \S$ induces a corresponding  transition $\gamma_1  \ltran{\alpha}{}{\S} \gamma_2$ with the same valuation $\rho$. \hfill  $\Box$

\end{proof}


\medskip

\noindent \textbf{Lemma~\ref{lem:derivsdelta}.}
A pattern $\varphi$ is derivable for $\S$ if and only if $\varphi$ is derivable for $\S^{\Delta}$.



\begin{proof}
By definition, $\varphi \eqbydef \pattern{\pi}{\phi}$ is derivable for $\S$ means that $\Delta_\S(\varphi)$ is not the empty disjunction. This holds if and only if there exists 
a rule $\rrule{\pattern{\pi_l}{\phi_l}}{ \pattern{\pi_r}{\phi_r}} \in\S $ such that $\pi_l$ matches $\pi$. The proof is finished by noting that $\pi_l$ is also the left-hand side of the rule corresponding $\rrule{\pi_l}{\Delta_\S(\pi_l)} \in \S^\Delta$. \hfill $\Box$
\end{proof}

\medskip

\noindent\textbf{Theorem~\ref{th:rlsymbex}.}
If $\S$ is total and weakly well-defined, and $G$ is derivable for $\S$, then $\S \cup G \vdash \Delta_\S(G)$ implies $\S \models G$.

\begin{proof}
For all $i = 1,\ldots, n$ we  apply the
\textsf{[Transitivity]} rule with $\varphi''_i \eqbydef \Delta_\S(\varphi_i)$, and obtain:
$$\dfrac{\S \vdash_G \varphi_i \Rightarrow \Delta_\S(\varphi_i) \quad (\S \cup G) \vdash \Delta_\S(\varphi_i)  \Rightarrow \varphi'_i}{\S \vdash_G \varphi_i \Rightarrow \varphi'_i}$$
The first hypothesis: $S \vdash_G \varphi_i \Rightarrow \Delta_\S(\varphi_i)$  holds thanks to Theorem~\ref{lem:deriv} and Lemma~\ref{obs:totalcov}.
 The second one, $(\S \cup G) \vdash \Delta_\S(\varphi_i)  \Rightarrow \varphi'_i$ is a hypothesis of the theorem. Hence, we obtain $S \vdash_G \varphi_i \Rightarrow \varphi'_i$ for all $i = 1,\ldots, n$, i.e., 
$S \vdash_G G$.
 Then we obtain 
$S \vdash G$ by applying the derived rule \emph{Set Circularity} of RL
Finally, the soundness of $\vdash$ (with $\S$ weakly well defined) implies $\S \models G$.

\end{proof}
%
%\section*{Appendix B: Examples}
%\label{sec:appB}
%
%\subsection{Mechanism for applying circularities}
%\label{sec:appb}
%The \kcheck tool uses a semi-automatic labeling mechanism to avoid proving a reachability rule using its corresponding circularity. To explain this better, let us consider the case of the \texttt{while} statement of \IMP and the reachability rules shown in Section~\ref{sec:soundimpl} for \texttt{gcd} program (Figure~\ref{fig:gcd}). When proving the reachability rule for the \texttt{while} loop~(\ref{eq:specgcd2}) the tool can apply directly the circularity rule corresponding exactly to this reachability rule that was added to $\S+\G$. Obviously, this is not valid, since it proves a reachability rule by itself. To avoid this, we created a semi-automatic mechanism which prevents circularities to apply in their own proofs. While adding reachability rules $\varphi \Ra \varphi'$ in $\G$, the user annotates the code from $\varphi$ (the \texttt{while} loop in our example) with a label $l$. Thus, the rewrite rules generated from $\G$ can be applied only on labelled patterns, that is $l:$\texttt{while}. When starting the execution of $\varphi$ the label is removed, so it only contains the code for the \texttt{while} loop. Therefore, the circularity corresponding to the loop cannot be applied since it does not match $\varphi$. Of course, this is the intended behavior for the first iteration of the loop, when the tool applies only rules from $\S$, unrolls the loop and collects new path constraints. On the other hand, for the second iteration of the loop we want to apply the circularity, since we have already verified it. In this case, the user has to put the same label $l$ at the end of \texttt{while} too, such that, after unrolling it once, the label gets before \texttt{while} and the circularity rules matches $l:$\texttt{while}. This labeling mechanism  ensures that the rules from $\S$ are applies before circularities and then gives priority to circularities in order to optimize the length of the proof.
%
%\subsection{Proving {\texttt gcd}}
%If the reachability rules (\ref{eq:specgcd}), (\ref{eq:specgcd2}), (\ref{eq:specgcd3}) needed for proving {\texttt gcd} are saved in a file {\small $\mathtt{gcd.rl}$} and the semantics of \IMP in {\small $\mathtt{imp.k}$} then we can call \kcheck as follows:
%%\vspace{-1ex}
%{\small
%\begin{verbatim}
%    $ kcheck imp.k -rlfile gcd.rl
%\end{verbatim}
%}
%%\vspace{-1ex}
%
%The tool generates the semantics $\S+\G$ and verifies the reachability rules from {\small $\mathtt{gcd.rl}$} one by one. The results are shown below:
%
%\noindent{\small
%\texttt{Verifying (0)...}\\
%%\texttt{Result:}\\
%\texttt{Solution 1, State 1:}\\
%\texttt{<path-condition>\\ $gcd(a, b) = gcd(x, y) \land y > 0 \land x >= 0 \land \lnot(y = 0)$\\ </path-condition>}\\
%\texttt{<k> $\kdot$ </k>\\
%<state> a $\mapsto$ $a$ b |-> $b$ r |-> $x'\%y'$ x |-> $y'$ y |-> $x'\%y'$ </state>
%}\\\\
%\texttt{Verifying (1)...}\\
%%\texttt{Result:}\\
%\texttt{Solution 1, State 3:}\\
%\texttt{<path-condition>\\
%   $gcd(a,b) = gcd(x, y) \land y >= 0 \land x >= 0 \land  \lnot (y <= 0) \land\\ 
%    gcd(a, b) = gcd(x, y) \land y > 0 \land x >= 0 \land\\
%    gcd(a, b) = gcd(symInt(1),symInt(2)) \land symInt(2) >= 0 \land symInt(1) >= 0 \land\\
%    gcd(a, b) = gcd(symInt(1), symInt(2)) \land symInt(2) >= 0 \land symInt(1) >= 0 \land\\ 
%    gcd (a,b ) = gcd (x', y') \land y' = 0 \land x' >= 0$\\ </path-condition>}\\
%\texttt{<k> $\kdot$ </k>\\
%<state> a $\mapsto$ $a$ b |-> $b$ r |-> $r'$ x |-> $x'$ y |-> $y'$ </state>
%}\\
%%<T>
%%    <k>
%%        .K
%%    </k>
%%    <state>
%%        a |-> #symInt(A)
%%        b |-> #symInt(B)
%%        r |-> #symInt(6)
%%        x |-> #symInt(4)
%%        y |-> #symInt(5)
%%    </state>
%%</T>
%%
%\texttt{Solution 2, State 4:}\\
%\texttt{<path-condition>\\
%    $gcd(a,b) = gcd(x, y) \land y >= 0 \land x >= 0 \land y <= 0$\\
%</path-condition>}\\
%\texttt{<k> $\kdot$ </k>\\
%<state> a $\mapsto$ $a$ b |-> $b$ r |-> $r$ x |-> $x$ y |-> $y$ </state>
%}\\
%%<T>
%%    <k>
%%        .K
%%    </k>
%%    <state>
%%        a |-> #symInt(A)
%%        b |-> #symInt(B)
%%        r |-> #symInt(R)
%%        x |-> #symInt(X)
%%        y |-> #symInt(Y)
%%    </state>
%%</T>
%%
%%
%\texttt{Verifying (2)...}\\
%%\texttt{Result:}\\
%\texttt{Solution 1, State 5:}\\
%\texttt{<path-condition>\\
%    $a >= 0 \land b >= 0 \land gcd(a, b) = gcd (a,b) \land\\
%     b >= 0 \land a >= 0 \land gcd(a , b) = gcd(x', y') \land\\
%     y' = 0 \land x' >= 0$\\
%</path-condition>}\\
%\texttt{<k> $\kdot$ </k>\\
%<state> a $\mapsto$ $a$ b |-> $b$ r |-> $r'$ x |-> $x'$ y |-> $y'$ </state>\\
%}
%%<T>
%%    <k>
%%        .K
%%    </k>
%%    <state>
%%        a |-> #symInt(A)
%%        b |-> #symInt(B)
%%        r |-> #symInt(9)
%%        x |-> #symInt(7)
%%        y |-> #symInt(8)
%%    </state>
%%</T>
%}
%The reachability rules are automatically numbered starting with 0, considering the order declared in the {\small $\mathtt{gcd.rl}$} file. In our case, the first verified reachability rule is (\ref{eq:specgcd3}). An empty \texttt{<k> $\kdot$ </k>} cell shows that the proof of this rule was successful. If the proof had failed then the cell would have contained the last configuration, which is the point where the proof got stuck. In the \texttt{<state>} cell we can  observe the effect of the executed code over the values of variables, \texttt{r} and \texttt{y} being mapped to $x\%y$, while \texttt{x} is mapped to $y$. The \texttt{<path-condition>} cell contains the formula collected during the symbolic execution of \texttt{body}. The constraints over $x$ and $y$ are collected from the initial condition given in the reachability rule $gcd(a, b) = gcd(x, y) \land y > 0 \land x >= 0$ and from the $\%$ operation condition, which is $\lnot(y = 0)$. For other rules, the path condition may include also formulas induced by circularities. The second output, which is the proof of (\ref{eq:specgcd2}), has two solutions corresponding to the cases when the loop condition holds or not. If the condition holds, then the rule (\ref{eq:specgcd3}) can be applied as circularity, thus adding its constraints to the current path condition. We can also observe that the path condition contains some symbolic values $symInt(1)$ and $symInt(2)$. Those are generated by the tool for variables which appear only in the right hand side of a reachability rule, when the circularity is applied. This helps users to write the reachability rules in a more uniform and elegant way. At the second iteration of the loop, (\ref{eq:specgcd2}) is applied as circularity, and thus it adds its own conditions to the path condition.
%The last proof corresponds to  (\ref{eq:specgcd}) and uses (\ref{eq:specgcd2}) as circularity. Since none of the proofs have failed then (\ref{eq:specgcd}) is proved successfully, so \texttt{gcd} is correct w.r.t. (\ref{eq:specgcd}).